def Contains {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] (P : α → β → Prop) (M : γ → δ → Prop) : Prop

Equations

• Contains P M = ∃ (f : α → γ), StrictMono f ∧ ∃ (g : β → δ), StrictMono g ∧ ∀ (a : α) (b : β), P a b → M (f a) (g b)

@[instance_reducible]

instance instDecidableContainsOfDecidableRelOfDecidableLTOfFintype {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] {P : α → β → Prop} {M : γ → δ → Prop} [DecidableRel P] [DecidableRel M] [DecidableLT α] [DecidableLT β] [DecidableLT γ] [DecidableLT δ] [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] : Decidable (Contains P M)

Equations

• One or more equations did not get rendered due to their size.

theorem contains_refl {γ : Type u_3} {δ : Type u_4} [LinearOrder γ] [LinearOrder δ] (M : γ → δ → Prop) : Contains M M

theorem contains_rfl {γ : Type u_3} {δ : Type u_4} [LinearOrder γ] [LinearOrder δ] {M : γ → δ → Prop} : Contains M M

@[simp]

theorem contains_of_isEmpty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] {P : α → β → Prop} {M : γ → δ → Prop} [IsEmpty α] [IsEmpty β] : Contains P M

theorem not_contains_false {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] (P : α → β → Prop) (P_nonempty : ∃ (a : α) (b : β), P a b) : ¬Contains P fun (x : γ) (x_1 : δ) => False