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
Instances For
    @[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
    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)
      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
      Instances For
        @[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.