Documentation

Mathlib.Order.RelIso.Set

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} [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
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
@[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
def Subrel {α : Type u_1} (r : ααProp) (p : Set α) :
ppProp

subrel r p is the inherited relation on a subset.

Equations
@[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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Subrel.relEmbedding_apply {α : Type u_1} (r : ααProp) (p : Set α) (a : p) :
(Subrel.relEmbedding r p).toEmbedding a = a
instance Subrel.instIsReflElemSubrel {α : Type u_1} (r : ααProp) [inst : IsRefl α r] (p : Set α) :
IsRefl (p) (Subrel r p)
Equations
instance Subrel.instIsSymmElemSubrel {α : Type u_1} (r : ααProp) [inst : IsSymm α r] (p : Set α) :
IsSymm (p) (Subrel r p)
Equations
instance Subrel.instIsTransElemSubrel {α : Type u_1} (r : ααProp) [inst : IsTrans α r] (p : Set α) :
IsTrans (p) (Subrel r p)
Equations
instance Subrel.instIsIrreflElemSubrel {α : Type u_1} (r : ααProp) [inst : 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.toEmbedding a p) :
r ↪r Subrel s p

Restrict the codomain of a relation embedding.

Equations
@[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 }