mathlib3 documentation

logic.embedding.set

Interactions between embeddings and sets. #

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

source
@[simp]
theorem equiv.as_embedding_range {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α ≃ subtype p) :
set.range ⇑(e.as_embedding) = set_of p
source
def function.embedding.coe_with_top {α : Type u_1} :
α ↪ with_top α

Embedding into with_top α.

Equations
source
@[simp]
theorem function.embedding.coe_with_top_apply {α : Type u_1} (ᾰ : α) :
⇑function.embedding.coe_with_top ᾰ = ↑ᾰ
source
def function.embedding.option_elim {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ set.range ⇑f) :
option α ↪ β

Given an embedding f : α ↪ β and a point outside of set.range f, construct an embedding option α ↪ β.

Equations
source
@[simp]
theorem function.embedding.option_elim_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ set.range ⇑f) (ᾰ : option α) :
⇑(f.option_elim x h) ᾰ = option.elim x ⇑f ᾰ
source
@[simp]
theorem function.embedding.option_embedding_equiv_apply_fst (α : Type u_1) (β : Type u_2) (f : option α ↪ β) :
(⇑(function.embedding.option_embedding_equiv α β) f).fst = function.embedding.coe_option.trans f
source
@[simp]
theorem function.embedding.option_embedding_equiv_symm_apply (α : Type u_1) (β : Type u_2) (f : Σ (f : α ↪ β), ↥(set.range ⇑f)ᶜ) :
⇑((function.embedding.option_embedding_equiv α β).symm) f = f.fst.option_elim ↑(f.snd) _
source
@[simp]
theorem function.embedding.option_embedding_equiv_apply_snd_coe (α : Type u_1) (β : Type u_2) (f : option α ↪ β) :
↑((⇑(function.embedding.option_embedding_equiv α β) f).snd) = ⇑f option.none
source
def function.embedding.option_embedding_equiv (α : Type u_1) (β : Type u_2) :
(option α ↪ β) ≃ Σ (f : α ↪ β), ↥(set.range ⇑f)ᶜ

Equivalence between embeddings of option α and a sigma type over the embeddings of α.

Equations
source
def function.embedding.cod_restrict {α : Sort u_1} {β : Type u_2} (p : set β) (f : α ↪ β) (H : ∀ (a : α), ⇑f a ∈ p) :
α ↪ ↥p

Restrict the codomain of an embedding.

Equations
source
@[simp]
theorem function.embedding.cod_restrict_apply {α : Sort u_1} {β : Type u_2} (p : set β) (f : α ↪ β) (H : ∀ (a : α), ⇑f a ∈ p) (a : α) :
⇑(function.embedding.cod_restrict p f H) a = ⟨⇑f a, _⟩
source
@[protected]
def function.embedding.image {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
set α ↪ set β

set.image as an embedding set α ↪ set β.

Equations
source
@[simp]
theorem function.embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : set α) :
⇑(f.image) s = ⇑f '' s
source
def set.embedding_of_subset {α : Type u_1} (s t : set α) (h : s ⊆ t) :
↥s ↪ ↥t

The injection map is an embedding between subsets.

Equations
source
@[simp]
theorem set.embedding_of_subset_apply {α : Type u_1} (s t : set α) (h : s ⊆ t) (x : ↥s) :
⇑(s.embedding_of_subset t h) x = ⟨x.val, _⟩
source
def subtype_or_equiv {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) :
{x // p x ∨ q x} ≃ {x // p x} ⊕ {x // q x}

A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop is equivalent to a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right, when disjoint p q.

See also equiv.sum_compl, for when is_compl p q.

Equations
source
@[simp]
theorem subtype_or_equiv_apply {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (ᾰ : {x // p x ∨ q x}) :
⇑(subtype_or_equiv p q h) ᾰ = ⇑(subtype_or_left_embedding p q) ᾰ
source
@[simp]
theorem subtype_or_equiv_symm_inl {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (x : {x // p x}) :
⇑((subtype_or_equiv p q h).symm) (sum.inl x) = ⟨↑x, _⟩
source
@[simp]
theorem subtype_or_equiv_symm_inr {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (x : {x // q x}) :
⇑((subtype_or_equiv p q h).symm) (sum.inr x) = ⟨↑x, _⟩