@[nolint]
structure
rel_hom
{α : Type u_4}
{β : Type u_5}
(r : α → α → Prop)
(s : β → β → Prop) :
Type (max u_4 u_5)
A relation homomorphism with respect to a given pair of relations r and s
is a function f : α → β such that r a b → s (f a) (f b).
@[instance]
def
rel_hom.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop} :
has_coe_to_fun (r →r s)
theorem
rel_hom.map_rel
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r →r s)
{a b : α}
(a_1 : r a b) :
theorem
rel_hom.coe_fn_inj
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
⦃e₁ e₂ : r →r s⦄
(a : ⇑e₁ = ⇑e₂) :
e₁ = e₂
The map coe_fn : (r →r s) → (α → β) is injective. We can't use function.injective
here but mimic its signature by using ⦃e₁ e₂⦄.
Identity map is a relation homomorphism.
@[simp]
A relation homomorphism is also a relation homomorphism between dual relations.
A function is a relation homomorphism from the preimage relation of s to s.
Equations
- rel_hom.preimage f s = {to_fun := f, map_rel' := _}
theorem
rel_hom.is_irrefl
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r →r s)
[is_irrefl β s] :
is_irrefl α r
theorem
rel_hom.is_asymm
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r →r s)
[is_asymm β s] :
is_asymm α r
theorem
rel_hom.well_founded
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r →r s)
(h : well_founded s) :
theorem
injective_of_increasing
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[is_trichotomous α r]
[is_irrefl β s]
(f : α → β)
(hf : ∀ {x y : α}, r x y → s (f x) (f y)) :
An increasing function is injective
theorem
rel_hom.injective_of_increasing
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
[is_trichotomous α r]
[is_irrefl β s]
(f : r →r s) :
An increasing function is injective
theorem
surjective.well_founded_iff
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
{f : α → β}
(hf : function.surjective f)
(o : ∀ {a b : α}, r a b ↔ s (f a) (f b)) :
structure
rel_embedding
{α : Type u_4}
{β : Type u_5}
(r : α → α → Prop)
(s : β → β → Prop) :
Type (max u_4 u_5)
- to_embedding : α ↪ β
- map_rel_iff' : ∀ {a b : α}, r a b ↔ s (⇑(c.to_embedding) a) (⇑(c.to_embedding) b)
A relation embedding with respect to a given pair of relations r and s
is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).
An order embedding is an embedding f : α ↪ β such that a ≤ b ↔ (f a) ≤ (f b).
This definition is an abbreviation of rel_embedding (≤) (≤).
def
subtype.rel_embedding
{X : Type u_1}
(r : X → X → Prop)
(p : X → Prop) :
subtype.val ⁻¹'o r ↪r r
The induced relation on a subtype is an embedding under the natural inclusion.
Equations
- subtype.rel_embedding r p = {to_embedding := {to_fun := subtype.val p, inj' := _}, map_rel_iff' := _}
theorem
preimage_equivalence
{α : Sort u_1}
{β : Sort u_2}
(f : α → β)
{s : β → β → Prop}
(hs : equivalence s) :
equivalence (f ⁻¹'o s)
def
rel_embedding.to_rel_hom
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s) :
r →r s
A relation embedding is also a relation homomorphism
Equations
- f.to_rel_hom = {to_fun := f.to_embedding.to_fun, map_rel' := _}
@[instance]
Equations
@[instance]
def
rel_embedding.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop} :
has_coe_to_fun (r ↪r s)
Equations
- rel_embedding.has_coe_to_fun = {F := λ (_x : r ↪r s), α → β, coe := λ (o : r ↪r s), ⇑(o.to_embedding)}
@[simp]
theorem
rel_embedding.to_rel_hom_eq_coe
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s) :
f.to_rel_hom = ↑f
theorem
rel_embedding.injective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s) :
@[simp]
theorem
rel_embedding.coe_fn_mk
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : α ↪ β)
(o : ∀ {a b : α}, r a b ↔ s (⇑f a) (⇑f b)) :
⇑{to_embedding := f, map_rel_iff' := o} = ⇑f
@[simp]
theorem
rel_embedding.coe_fn_to_embedding
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s) :
⇑(f.to_embedding) = ⇑f
theorem
rel_embedding.coe_fn_inj
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
⦃e₁ e₂ : r ↪r s⦄
(a : ⇑e₁ = ⇑e₂) :
e₁ = e₂
The map coe_fn : (r ↪r s) → (α → β) is injective. We can't use function.injective
here but mimic its signature by using ⦃e₁ e₂⦄.
Identity map is a relation embedding.
Equations
- rel_embedding.refl r = {to_embedding := function.embedding.refl α, map_rel_iff' := _}
def
rel_embedding.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → α → Prop}
{s : β → β → Prop}
{t : γ → γ → Prop}
(f : r ↪r s)
(g : s ↪r t) :
r ↪r t
Composition of two relation embeddings is a relation embedding.
Equations
- f.trans g = {to_embedding := f.to_embedding.trans g.to_embedding, map_rel_iff' := _}
@[simp]
theorem
rel_embedding.refl_apply
{α : Type u_1}
{r : α → α → Prop}
(x : α) :
⇑(rel_embedding.refl r) x = x
def
rel_embedding.swap
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s) :
A relation embedding is also a relation embedding between dual relations.
Equations
- f.swap = {to_embedding := f.to_embedding, map_rel_iff' := _}
If f is injective, then it is a relation embedding from the
preimage relation of s to s.
Equations
- rel_embedding.preimage f s = {to_embedding := f, map_rel_iff' := _}
theorem
rel_embedding.is_irrefl
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_irrefl β s] :
is_irrefl α r
theorem
rel_embedding.is_refl
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_refl β s] :
is_refl α r
theorem
rel_embedding.is_symm
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_symm β s] :
is_symm α r
theorem
rel_embedding.is_asymm
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_asymm β s] :
is_asymm α r
theorem
rel_embedding.is_antisymm
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_antisymm β s] :
is_antisymm α r
theorem
rel_embedding.is_trans
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_trans β s] :
is_trans α r
theorem
rel_embedding.is_total
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_total β s] :
is_total α r
theorem
rel_embedding.is_preorder
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_preorder β s] :
is_preorder α r
theorem
rel_embedding.is_partial_order
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_partial_order β s] :
is_partial_order α r
theorem
rel_embedding.is_linear_order
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_linear_order β s] :
is_linear_order α r
theorem
rel_embedding.is_strict_order
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_strict_order β s] :
is_strict_order α r
theorem
rel_embedding.is_trichotomous
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_trichotomous β s] :
is_trichotomous α r
theorem
rel_embedding.is_strict_total_order'
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_strict_total_order' β s] :
theorem
rel_embedding.well_founded
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
(h : well_founded s) :
theorem
rel_embedding.is_well_order
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
[is_well_order β s] :
is_well_order α r
def
rel_embedding.of_monotone
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
[is_trichotomous α r]
[is_asymm β s]
(f : α → β)
(H : ∀ (a b : α), r a b → s (f a) (f b)) :
r ↪r s
It suffices to prove f is monotone between strict relations
to show it is a relation embedding.
Equations
- rel_embedding.of_monotone f H = {to_embedding := {to_fun := f, inj' := _}, map_rel_iff' := _}
@[simp]
theorem
rel_embedding.of_monotone_coe
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
[is_trichotomous α r]
[is_asymm β s]
(f : α → β)
(H : ∀ (a b : α), r a b → s (f a) (f b)) :
⇑(rel_embedding.of_monotone f H) = f
def
rel_embedding.order_embedding_of_lt_embedding
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
(f : has_lt.lt ↪r has_lt.lt) :
α ↪o β
Embeddings of partial orders that preserve < also preserve ≤
Equations
- f.order_embedding_of_lt_embedding = {to_embedding := f.to_embedding, map_rel_iff' := _}
def
order_embedding.lt_embedding
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ↪o β) :
lt is preserved by order embeddings of preorders
Equations
- f.lt_embedding = {to_embedding := f.to_embedding, map_rel_iff' := _}
@[simp]
theorem
order_embedding.lt_embedding_apply
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ↪o β)
(x : α) :
⇑(f.lt_embedding) x = ⇑f x
theorem
order_embedding.well_founded
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ↪o β)
(a : well_founded has_lt.lt) :
theorem
order_embedding.is_well_order
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ↪o β)
[is_well_order β has_lt.lt] :
def
order_embedding.dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ↪o β) :
order_dual α ↪o order_dual β
An order embedding is also an order embedding between dual orders.
Equations
- f.dual = {to_embedding := f.to_embedding, map_rel_iff' := _}
The inclusion map fin n → ℕ is a relation embedding.
Equations
- fin.val.rel_embedding n = {to_embedding := {to_fun := coe coe_to_lift, inj' := _}, map_rel_iff' := _}
The inclusion map fin m → fin n is an order embedding.
Equations
- fin_fin.rel_embedding h = {to_embedding := {to_fun := λ (_x : fin m), fin_fin.rel_embedding._match_1 h _x, inj' := _}, map_rel_iff' := _}
- fin_fin.rel_embedding._match_1 h ⟨x, h'⟩ = ⟨x, _⟩
@[instance]
The ordering on fin n is a well order.
def
rel_iso.to_rel_embedding
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ≃r s) :
r ↪r s
Convert an rel_iso to an rel_embedding. This function is also available as a coercion
but often it is easier to write f.to_rel_embedding than to write explicitly r and s
in the target type.
Equations
- f.to_rel_embedding = {to_embedding := f.to_equiv.to_embedding, map_rel_iff' := _}
@[instance]
Equations
@[instance]
def
rel_iso.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop} :
has_coe_to_fun (r ≃r s)
@[simp]
theorem
rel_iso.to_rel_embedding_eq_coe
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ≃r s) :
f.to_rel_embedding = ↑f
theorem
rel_iso.to_equiv_injective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop} :
theorem
rel_iso.coe_fn_injective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
⦃e₁ e₂ : r ≃r s⦄
(h : ⇑e₁ = ⇑e₂) :
e₁ = e₂
The map coe_fn : (r ≃r s) → (α → β) is injective. We can't use function.injective
here but mimic its signature by using ⦃e₁ e₂⦄.
Identity map is a relation isomorphism.
Equations
- rel_iso.refl r = {to_equiv := equiv.refl α, map_rel_iff' := _}
def
rel_iso.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → α → Prop}
{s : β → β → Prop}
{t : γ → γ → Prop}
(f₁ : r ≃r s)
(f₂ : s ≃r t) :
r ≃r t
Composition of two relation isomorphisms is a relation isomorphism.
a relation isomorphism is also a relation isomorphism between dual relations.
@[simp]
theorem
rel_iso.bijective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(e : r ≃r s) :
theorem
rel_iso.injective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(e : r ≃r s) :
theorem
rel_iso.surjective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(e : r ≃r s) :
Any equivalence lifts to a relation isomorphism between s and its preimage.
Equations
- rel_iso.preimage f s = {to_equiv := f, map_rel_iff' := _}
def
rel_iso.of_surjective
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
(H : function.surjective ⇑f) :
r ≃r s
A surjective relation embedding is a relation isomorphism.
Equations
- rel_iso.of_surjective f H = {to_equiv := equiv.of_bijective ⇑f _, map_rel_iff' := _}
@[simp]
theorem
rel_iso.of_surjective_coe
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(f : r ↪r s)
(H : function.surjective ⇑f) :
⇑(rel_iso.of_surjective f H) = ⇑f
def
rel_iso.sum_lex_congr
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{r₁ : α₁ → α₁ → Prop}
{r₂ : α₂ → α₂ → Prop}
{s₁ : β₁ → β₁ → Prop}
{s₂ : β₂ → β₂ → Prop}
(e₁ : r₁ ≃r r₂)
(e₂ : s₁ ≃r s₂) :
Equations
- e₁.sum_lex_congr e₂ = {to_equiv := e₁.to_equiv.sum_congr e₂.to_equiv, map_rel_iff' := _}
def
rel_iso.prod_lex_congr
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{r₁ : α₁ → α₁ → Prop}
{r₂ : α₂ → α₂ → Prop}
{s₁ : β₁ → β₁ → Prop}
{s₂ : β₂ → β₂ → Prop}
(e₁ : r₁ ≃r r₂)
(e₂ : s₁ ≃r s₂) :
Equations
- e₁.prod_lex_congr e₂ = {to_equiv := e₁.to_equiv.prod_congr e₂.to_equiv, map_rel_iff' := _}
@[instance]
Equations
- rel_iso.group = {mul := λ (f₁ f₂ : r ≃r r), f₂.trans f₁, mul_assoc := _, one := rel_iso.refl r, one_mul := _, mul_one := _, inv := rel_iso.symm r, mul_left_inv := _}
A subset p : set α embeds into α
Equations
- set_coe_embedding p = {to_fun := subtype.val (λ (x : α), x ∈ p), inj' := _}
Equations
- subrel.rel_embedding r p = {to_embedding := set_coe_embedding p, map_rel_iff' := _}
@[simp]
theorem
subrel.rel_embedding_apply
{α : Type u_1}
(r : α → α → Prop)
(p : set α)
(a : ↥p) :
⇑(subrel.rel_embedding r p) a = a.val
@[instance]
def
subrel.is_well_order
{α : Type u_1}
(r : α → α → Prop)
[is_well_order α r]
(p : set α) :
is_well_order ↥p (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) :
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' := _}
def
order_iso.dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α ≃o β) :
order_dual α ≃o order_dual β
An order isomorphism is also an order isomorphism between dual orders.
theorem
rel_embedding.map_inf_le
{α : Type u_1}
{β : Type u_2}
{a₁ a₂ : α}
[semilattice_inf α]
[semilattice_inf β]
(f : α ↪o β) :
theorem
rel_iso.map_inf
{α : Type u_1}
{β : Type u_2}
{a₁ a₂ : α}
[semilattice_inf α]
[semilattice_inf β]
(f : α ≃o β) :
theorem
rel_embedding.le_map_sup
{α : Type u_1}
{β : Type u_2}
{a₁ a₂ : α}
[semilattice_sup α]
[semilattice_sup β]
(f : α ↪o β) :
theorem
rel_iso.map_sup
{α : Type u_1}
{β : Type u_2}
{a₁ a₂ : α}
[semilattice_sup α]
[semilattice_sup β]
(f : α ≃o β) :