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.

ink

theorem RelHomClass.map_inf {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : SemilatticeInf α] [inst : LinearOrder β] [inst : 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

ink

theorem RelHomClass.map_sup {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : SemilatticeSup α] [inst : LinearOrder β] [inst : 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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

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

ink

@[simp]

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

ink

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

Equations

• @Subrel.instIsWellOrderElemSubrel = @Subrel.instIsWellOrderElemSubrel.proof_1

ink

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

Equations

• @Subrel.instIsReflElemSubrel = @Subrel.instIsReflElemSubrel.proof_1

ink

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

Equations

• @Subrel.instIsSymmElemSubrel = @Subrel.instIsSymmElemSubrel.proof_1

ink

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

Equations

• @Subrel.instIsTransElemSubrel = @Subrel.instIsTransElemSubrel.proof_1

ink

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

Equations

• @Subrel.instIsIrreflElemSubrel = @Subrel.instIsIrreflElemSubrel.proof_1

ink

def RelEmbedding.codRestrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ↪r s) (H : ∀ (a : α), ↑f.toEmbedding 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' := (_ : ∀ {a b : α}, s (↑f.toEmbedding a) (↑f.toEmbedding b) ↔ r a b) }

ink

@[simp]

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