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_5} [SemilatticeInf α] [LinearOrder β] [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_5} [SemilatticeSup α] [LinearOrder β] [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 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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Subrel.relEmbedding_apply {α : Type u_1} (r : ααProp) (p : Set α) (a : p) :
      ↑(Subrel.relEmbedding r p) a = a
      instance Subrel.instIsReflElemSubrel {α : Type u_1} (r : ααProp) [IsRefl α r] (p : Set α) :
      IsRefl (p) (Subrel r p)
      Equations
      instance Subrel.instIsSymmElemSubrel {α : Type u_1} (r : ααProp) [IsSymm α r] (p : Set α) :
      IsSymm (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 = { val := f a, property := H a }