mathlib3 documentation

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} [semilattice_inf α] [linear_order β] [rel_hom_class F has_lt.lt has_lt.lt] (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} [semilattice_sup α] [linear_order β] [rel_hom_class F gt 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
Instances for subrel
@[simp]
theorem subrel_val {α : Type u_1} (r : α α Prop) (p : set α) {a b : p} :
subrel r p a b r a.val b.val
@[protected]
def subrel.rel_embedding {α : Type u_1} (r : α α Prop) (p : set α) :
subrel r 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) :
@[protected, instance]
def subrel.is_well_order {α : Type u_1} (r : α α Prop) [is_well_order α r] (p : set α) :
@[protected, instance]
def subrel.is_refl {α : Type u_1} (r : α α Prop) [is_refl α r] (p : set α) :
@[protected, instance]
def subrel.is_symm {α : Type u_1} (r : α α Prop) [is_symm α r] (p : set α) :
@[protected, instance]
def subrel.is_trans {α : Type u_1} (r : α α Prop) [is_trans α r] (p : set α) :
@[protected, instance]
def subrel.is_irrefl {α : Type u_1} (r : α α Prop) [is_irrefl α r] (p : set α) :
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 subrel s 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 : α) :