# 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} [] [] [FunLike F β α] [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} [] [] [FunLike F β α] [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.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) :
() a = a
instance Subrel.instIsWellOrderElem {α : Type u_1} (r : ααProp) [] (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 : α) :
() a = f a,
theorem RelIso.image_eq_preimage_symm {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (e : r ≃r s) (t : Set α) :
e '' t = e.symm ⁻¹' t
theorem RelIso.preimage_eq_image_symm {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (e : r ≃r s) (t : Set β) :
e ⁻¹' t = e.symm '' t