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_5} [SemilatticeInf α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x x_1 : β) => x < x_1) fun (x x_1 : α) => x < x_1] (a : F) (m : β) (n : β) : a (m ⊓ n) = a m ⊓ a n

theorem RelHomClass.map_sup {α : Type u_1} {β : Type u_2} {F : Type u_5} [SemilatticeSup α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x x_1 : β) => x > x_1) fun (x x_1 : α) => x > x_1] (a : F) (m : β) (n : β) : a (m ⊔ n) = a m ⊔ a n

@[simp]

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 : Set α) : ↑p → ↑p → Prop

Subrel r p is the inherited relation on a subset.

Equations

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

Instances For

• Subrel.instIsIrreflElem
• Subrel.instIsReflElem
• Subrel.instIsSymmElem
• Subrel.instIsTransElem
• Subrel.instIsWellOrderElem

@[simp]

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

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

The relation embedding from the inherited relation on a subset.

Equations

• Subrel.relEmbedding r p = { toEmbedding := Function.Embedding.subtype fun (x : α) => x ∈ p, map_rel_iff' := ⋯ }

@[simp]

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

instance Subrel.instIsWellOrderElem {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] (p : Set α) : IsWellOrder (↑p) (Subrel r p)

Equations

• ⋯ = ⋯

instance Subrel.instIsReflElem {α : Type u_1} (r : α → α → Prop) [IsRefl α r] (p : Set α) : IsRefl (↑p) (Subrel r p)

Equations

• ⋯ = ⋯

instance Subrel.instIsSymmElem {α : Type u_1} (r : α → α → Prop) [IsSymm α r] (p : Set α) : IsSymm (↑p) (Subrel r p)

Equations

• ⋯ = ⋯

instance Subrel.instIsTransElem {α : Type u_1} (r : α → α → Prop) [IsTrans α r] (p : Set α) : IsTrans (↑p) (Subrel r p)

Equations

• ⋯ = ⋯

instance Subrel.instIsIrreflElem {α : Type u_1} (r : α → α → Prop) [IsIrrefl α r] (p : Set α) : IsIrrefl (↑p) (Subrel r p)

Equations

• ⋯ = ⋯

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 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 : α) : (RelEmbedding.codRestrict p f H) a = ⟨f a, ⋯⟩

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

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