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} [SemilatticeInf α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x1 x2 : β) => x1 < x2) fun (x1 x2 : α) => x1 < x2] (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} [SemilatticeSup α] [LinearOrder β] [FunLike F β α] [RelHomClass F (fun (x1 x2 : β) => x1 > x2) fun (x1 x2 : α) => x1 > x2] (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 α) :
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
@[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
@[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_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (t : Set α) :
e '' t = e.symm ⁻¹' t
theorem RelIso.preimage_eq_image_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (t : Set β) :
e ⁻¹' t = e.symm '' t
theorem Acc.of_subrel {α : Type u_1} {r : ααProp} [IsTrans α r] {b : α} (a : { a : α // r a b }) (h : Acc (Subrel r {a : α | r a b}) a) :
Acc r a
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.