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 : β)
:
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 : β)
:
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' := ⋯ }
Instances For
@[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)
instance
Subrel.instIsWellOrderSubtypeSetOf
{α : Type u_1}
(r : α → α → Prop)
(p : α → Prop)
[IsWellOrder α r]
:
IsWellOrder { a : α // p a } (Subrel r {a : α | p a})
def
RelEmbedding.codRestrict
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(p : Set β)
(f : r ↪r s)
(H : ∀ (a : α), f 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' := ⋯ }
Instances For
theorem
wellFounded_iff_wellFounded_subrel
{α : Type u_1}
{r : α → α → Prop}
[IsTrans α r]
:
WellFounded r ↔ ∀ (b : α), WellFounded (Subrel r {a : α | r a b})
A relation r
is well-founded iff every downward-interval { a | r a b }
of it is
well-founded.