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 : β)
:
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 : β)
:
@[simp]
theorem
Subrel.relEmbedding_apply
{α : Type u_1}
(r : α → α → Prop)
(p : Set α)
(a : ↑p)
:
↑(Subrel.relEmbedding r p).toEmbedding a = ↑a
instance
Subrel.instIsWellOrderElemSubrel
{α : Type u_1}
(r : α → α → Prop)
[inst : IsWellOrder α r]
(p : Set α)
:
IsWellOrder (↑p) (Subrel r p)
instance
Subrel.instIsReflElemSubrel
{α : Type u_1}
(r : α → α → Prop)
[inst : IsRefl α r]
(p : Set α)
:
instance
Subrel.instIsSymmElemSubrel
{α : Type u_1}
(r : α → α → Prop)
[inst : IsSymm α r]
(p : Set α)
:
instance
Subrel.instIsTransElemSubrel
{α : Type u_1}
(r : α → α → Prop)
[inst : IsTrans α r]
(p : Set α)
:
instance
Subrel.instIsIrreflElemSubrel
{α : Type u_1}
(r : α → α → Prop)
[inst : IsIrrefl α r]
(p : Set α)
:
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)
:
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) }