def
Contains
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[LinearOrder α]
[LinearOrder β]
[LinearOrder γ]
[LinearOrder δ]
(P : α → β → Prop)
(M : γ → δ → Prop)
:
Equations
- Contains P M = ∃ (f : α → γ), StrictMono f ∧ ∃ (g : β → δ), StrictMono g ∧ ∀ (a : α) (b : β), P a b → M (f a) (g b)
Instances For
@[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 δ]
:
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)
: