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.

@[simp]
theorem equiv.as_embedding_range {α : Sort u_1} {β : Type u_2} {p : β Prop} (e : α subtype p) :
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
@[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
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
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
@[simp]
theorem function.embedding.cod_restrict_apply {α : Sort u_1} {β : Type u_2} (p : set β) (f : α β) (H : (a : α), f a p) (a : α) :
@[protected]
def function.embedding.image {α : Type u_1} {β : Type u_2} (f : α β) :
set α set β

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

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

The injection map is an embedding between subsets.

Equations
@[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, _⟩
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
@[simp]
theorem subtype_or_equiv_apply {α : Type u_1} (p q : α Prop) [decidable_pred p] (h : disjoint p q) (ᾰ : {x // p x q x}) :
@[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, _⟩
@[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, _⟩