# 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} [] [] [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} [] [] [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.

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.

Instances For
@[simp]
theorem Subrel.relEmbedding_apply {α : Type u_1} (r : ααProp) (p : Set α) (a : p) :
↑() a = a
instance Subrel.instIsWellOrderElemSubrel {α : Type u_1} (r : ααProp) [] (p : Set α) :
IsWellOrder (p) (Subrel r p)
instance Subrel.instIsReflElemSubrel {α : Type u_1} (r : ααProp) [IsRefl α r] (p : Set α) :
IsRefl (p) (Subrel r p)
instance Subrel.instIsSymmElemSubrel {α : Type u_1} (r : ααProp) [IsSymm α r] (p : Set α) :
IsSymm (p) (Subrel r p)
instance Subrel.instIsTransElemSubrel {α : Type u_1} (r : ααProp) [IsTrans α r] (p : Set α) :
IsTrans (p) (Subrel r p)
instance Subrel.instIsIrreflElemSubrel {α : Type u_1} (r : ααProp) [IsIrrefl α r] (p : Set α) :
IsIrrefl (p) (Subrel r p)
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.

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 = { val := f a, property := H a }