Interactions between relation homomorphisms and sets

It is likely that there are better homes for many of these statement, in files further down the import graph.

theorem RelHomClass.map_inf {α : Type u_1} {β : Type u_2} {F : Type u_3} [SemilatticeInf α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x1 x2 : β) => x1 < x2) fun (x1 x2 : α) => x1 < x2] (a : F) (m n : β) : a (min m n) = a m ⊓ a n

theorem RelHomClass.map_sup {α : Type u_1} {β : Type u_2} {F : Type u_3} [SemilatticeSup α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x1 x2 : β) => x1 > x2) fun (x1 x2 : α) => x1 > x2] (a : F) (m n : β) : a (max m n) = a m ⊔ a n

theorem RelHomClass.directed {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_3} [FunLike F α β] [RelHomClass F r s] {ι : Sort u_4} {a : ι → α} {f : F} (ha : Directed r a) : Directed s (⇑f ∘ a)

theorem RelHomClass.directedOn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_3} [FunLike F α β] [RelHomClass F r s] {f : F} {t : Set α} (hs : DirectedOn r t) : DirectedOn s (⇑f '' t)

theorem RelIso.range_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : Set.range ⇑e = Set.univ

def Subrel {α : Type u_1} (r : α → α → Prop) (p : α → Prop) : Subtype p → Subtype p → Prop

Subrel r p is the inherited relation on a subtype.

We could also consider a Set.Subrel r s variant for dot notation, but this ends up interacting poorly with simpNF.

Equations

• Subrel r p = Subtype.val ⁻¹'o r

@[simp]

theorem subrel_val {α : Type u_1} (r : α → α → Prop) (p : α → Prop) {a b : Subtype p} : Subrel r p a b ↔ r ↑a ↑b

def Subrel.relEmbedding {α : Type u_1} (r : α → α → Prop) (p : α → Prop) : Subrel r p ↪r r

The relation embedding from the inherited relation on a subset.

Equations

• Subrel.relEmbedding r p = { toEmbedding := Function.Embedding.subtype p, map_rel_iff' := ⋯ }

@[simp]

theorem Subrel.relEmbedding_apply {α : Type u_1} (r : α → α → Prop) (p : α → Prop) (a : Subtype p) : (Subrel.relEmbedding r p) a = ↑a

def Subrel.inclusionEmbedding {α : Type u_1} (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) : (Subrel r fun (x : α) => x ∈ s) ↪r Subrel r fun (x : α) => x ∈ t

Set.inclusion as a relation embedding.

Equations

• Subrel.inclusionEmbedding r h = { toFun := Set.inclusion h, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Subrel.coe_inclusionEmbedding {α : Type u_1} (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) : ⇑(Subrel.inclusionEmbedding r h) = Set.inclusion h

instance Subrel.instReflSubtype {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (p : α → Prop) : Std.Refl (Subrel r p)

instance Subrel.instSymmSubtype {α : Type u_1} (r : α → α → Prop) [Std.Symm r] (p : α → Prop) : Std.Symm (Subrel r p)

instance Subrel.instAsymmSubtype {α : Type u_1} (r : α → α → Prop) [Std.Asymm r] (p : α → Prop) : Std.Asymm (Subrel r p)

instance Subrel.instIsTransSubtype {α : Type u_1} (r : α → α → Prop) [IsTrans α r] (p : α → Prop) : IsTrans (Subtype p) (Subrel r p)

instance Subrel.instIrreflSubtype {α : Type u_1} (r : α → α → Prop) [Std.Irrefl r] (p : α → Prop) : Std.Irrefl (Subrel r p)

instance Subrel.instTrichotomousSubtype {α : Type u_1} (r : α → α → Prop) [Std.Trichotomous r] (p : α → Prop) : Std.Trichotomous (Subrel r p)

instance Subrel.instWellFoundedSubtype {α : Type u_1} (r : α → α → Prop) [WellFounded r] (p : α → Prop) : WellFounded (Subrel r p)

instance Subrel.instIsPreorderSubtype {α : Type u_1} (r : α → α → Prop) [IsPreorder α r] (p : α → Prop) : IsPreorder (Subtype p) (Subrel r p)

instance Subrel.instIsStrictOrderSubtype {α : Type u_1} (r : α → α → Prop) [IsStrictOrder α r] (p : α → Prop) : IsStrictOrder (Subtype p) (Subrel r p)

instance Subrel.instIsWellOrderSubtype {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] (p : α → Prop) : IsWellOrder (Subtype p) (Subrel r p)

def RelIso.subrelUnivIso {α : Type u_1} {r : α → α → Prop} {p : α → Prop} (h : ∀ (x : α), p x) : Subrel r p ≃r r

If a proposition holds for all elements, then the Subrel is equivalent to the original relation.

Equations

• RelIso.subrelUnivIso h = { toEquiv := Equiv.subtypeUnivEquiv h, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.subrelUnivIso_apply {α : Type u_1} {r : α → α → Prop} {p : α → Prop} (h : ∀ (x : α), p x) (x : Subtype p) : (subrelUnivIso h) x = ↑x

@[simp]

theorem RelIso.subrelUnivIso_symm_apply {α : Type u_1} {r : α → α → Prop} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) : (subrelUnivIso h).symm x = ⟨x, ⋯⟩

def RelEmbedding.codRestrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ↪r s) (H : ∀ (a : α), f a ∈ p) : r ↪r Subrel s fun (x : β) => x ∈ p

Restrict the codomain of a relation embedding.

Equations

• RelEmbedding.codRestrict p f H = { toEmbedding := Function.Embedding.codRestrict p f.toEmbedding H, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ↪r s) (H : ∀ (a : α), f a ∈ p) (a : α) : (codRestrict p f H) a = ⟨f a, ⋯⟩

theorem RelIso.image_eq_preimage_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (t : Set α) : ⇑e '' t = ⇑e.symm ⁻¹' t

theorem RelIso.preimage_eq_image_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (t : Set β) : ⇑e ⁻¹' t = ⇑e.symm '' t

theorem Acc.of_subrel {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {b : α} (a : { a : α // r a b }) (h : Acc (Subrel r fun (x : α) => r x b) a) : Acc r ↑a

theorem wellFounded_iff_wellFounded_subrel {α : Type u_1} {r : α → α → Prop} [IsTrans α r] : WellFounded r ↔ ∀ (b : α), WellFounded (Subrel r fun (x : α) => r x b)

A relation r is well-founded iff every downward-interval { a | r a b } of it is well-founded.