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

source

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

source

@[simp]

theorem rel_iso.range_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :

set.range ⇑e = set.univ

source

def subrel {α : Type u_1} (r : α → α → Prop) (p : set α) :

↥p → ↥p → Prop

subrel r p is the inherited relation on a subset.

Equations

subrel r p = coe ⁻¹'o r

Instances for subrel

source

@[simp]

theorem subrel_val {α : Type u_1} (r : α → α → Prop) (p : set α) {a b : ↥p} :

subrel r p a b ↔ r a.val b.val

source

@[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

subrel.rel_embedding r p = {to_embedding := function.embedding.subtype (λ (x : α), x ∈ p), map_rel_iff' := _}

source

@[simp]

theorem subrel.rel_embedding_apply {α : Type u_1} (r : α → α → Prop) (p : set α) (a : ↥p) :

⇑(subrel.rel_embedding r p) a = a.val

source

@[protected, instance]

def subrel.is_well_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (p : set α) :

is_well_order ↥p (subrel r p)

source

@[protected, instance]

def subrel.is_refl {α : Type u_1} (r : α → α → Prop) [is_refl α r] (p : set α) :

is_refl ↥p (subrel r p)

source

@[protected, instance]

def subrel.is_symm {α : Type u_1} (r : α → α → Prop) [is_symm α r] (p : set α) :

is_symm ↥p (subrel r p)

source

@[protected, instance]

def subrel.is_trans {α : Type u_1} (r : α → α → Prop) [is_trans α r] (p : set α) :

is_trans ↥p (subrel r p)

source

@[protected, instance]

def subrel.is_irrefl {α : Type u_1} (r : α → α → Prop) [is_irrefl α r] (p : set α) :

is_irrefl ↥p (subrel r p)

source

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

rel_embedding.cod_restrict p f H = {to_embedding := function.embedding.cod_restrict p f.to_embedding H, map_rel_iff' := _}

source

@[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 : α) :

⇑(rel_embedding.cod_restrict p f H) a = ⟨⇑f a, _⟩