Interactions between embeddings and sets. #
@[simp]
theorem
Function.Embedding.optionEmbeddingEquiv_apply_fst
(α : Type u_1)
(β : Type u_2)
(f : Option α ↪ β)
:
@[simp]
theorem
Function.Embedding.optionEmbeddingEquiv_apply_snd_coe
(α : Type u_1)
(β : Type u_2)
(f : Option α ↪ β)
:
@[simp]
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.sumCompl
, for when IsCompl p q
.
Equations
Instances For
@[simp]
theorem
subtypeOrEquiv_apply
{α : Type u_1}
(p q : α → Prop)
[DecidablePred p]
(h : Disjoint p q)
(a : { x : α // p x ∨ q x })
:
@[simp]
theorem
Function.Embedding.sumSet_apply
{α : Type u_1}
{s t : Set α}
(h : Disjoint s t)
(a✝ : ↑s ⊕ ↑t)
: