# mathlib3documentation

order.rel_iso.set

# Interactions between relation homomorphisms and sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

It is likely that there are better homes for many of these statement, in files further down the import graph.

theorem rel_hom_class.map_inf {α : Type u_1} {β : Type u_2} {F : Type u_5} [linear_order β] (a : F) (m n : β) :
a (m n) = a m a n
theorem rel_hom_class.map_sup {α : Type u_1} {β : Type u_2} {F : Type u_5} [linear_order β] [ gt] (a : F) (m n : β) :
a (m n) = a m a n
@[simp]
theorem rel_iso.range_eq {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (e : r ≃r s) :
def subrel {α : Type u_1} (r : α α Prop) (p : set α) :
p p Prop

subrel r p is the inherited relation on a subset.

Equations
• p =
Instances for subrel
@[simp]
theorem subrel_val {α : Type u_1} (r : α α Prop) (p : set α) {a b : p} :
p a b r a.val b.val
@[protected]
def subrel.rel_embedding {α : Type u_1} (r : α α Prop) (p : set α) :
p ↪r r

The relation embedding from the inherited relation on a subset.

Equations
@[simp]
theorem subrel.rel_embedding_apply {α : Type u_1} (r : α α Prop) (p : set α) (a : p) :
p) a = a.val
@[protected, instance]
def subrel.is_well_order {α : Type u_1} (r : α α Prop) [ r] (p : set α) :
(subrel r p)
@[protected, instance]
def subrel.is_refl {α : Type u_1} (r : α α Prop) [ r] (p : set α) :
(subrel r p)
@[protected, instance]
def subrel.is_symm {α : Type u_1} (r : α α Prop) [ r] (p : set α) :
(subrel r p)
@[protected, instance]
def subrel.is_trans {α : Type u_1} (r : α α Prop) [ r] (p : set α) :
(subrel r p)
@[protected, instance]
def subrel.is_irrefl {α : Type u_1} (r : α α Prop) [ r] (p : set α) :
(subrel r p)
def rel_embedding.cod_restrict {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : r ↪r s) (H : (a : α), f a p) :
r ↪r p

Restrict the codomain of a relation embedding.

Equations
@[simp]
theorem rel_embedding.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : r ↪r s) (H : (a : α), f a p) (a : α) :
H) a = f a, _⟩