Equivalences for Option α
#
We define
Equiv.optionCongr
: theOption α ≃ Option β≃ Option β
constructed frome : α ≃ β≃ β
by sendingnone
tonone
, and applyinge
elsewhere.Equiv.removeNone
: theα ≃ β≃ β
constructed fromOption α ≃ Option β≃ Option β
by removingnone
from both sides.
@[simp]
theorem
Equiv.optionCongr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
:
∀ (a : Option α), ↑(Equiv.optionCongr e) a = Option.map (↑e) a
@[simp]
theorem
Equiv.optionCongr_refl
{α : Type u_1}
:
Equiv.optionCongr (Equiv.refl α) = Equiv.refl (Option α)
@[simp]
@[simp]
theorem
Equiv.optionCongr_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(e₁ : α ≃ β)
(e₂ : β ≃ γ)
:
Equiv.trans (Equiv.optionCongr e₁) (Equiv.optionCongr e₂) = Equiv.optionCongr (Equiv.trans e₁ e₂)
When α
and β
are in the same universe, this is the same as the result of
EquivFunctor.mapEquiv
.
If we have a value on one side of an Equiv
of Option
we also have a value on the other side of the equivalence
Equations
- Equiv.removeNone_aux e x = if h : Option.isSome (↑e (some x)) = true then Option.get (↑e (some x)) h else Option.get (↑e none) (_ : Option.isSome (↑e none) = true)
theorem
Equiv.removeNone_aux_inv
{α : Type u_1}
{β : Type u_2}
(e : Option α ≃ Option β)
(x : α)
:
Equiv.removeNone_aux (Equiv.symm e) (Equiv.removeNone_aux e x) = x
theorem
Equiv.some_removeNone_iff
{α : Type u_2}
{β : Type u_1}
(e : Option α ≃ Option β)
{x : α}
:
some (↑(Equiv.removeNone e) x) = ↑e none ↔ ↑(Equiv.symm e) none = some x
@[simp]
theorem
Equiv.optionCongr_injective
{α : Type u_1}
{β : Type u_2}
:
Function.Injective Equiv.optionCongr
Equivalences between Option α
and β
that send none
to x
are equivalent to
equivalences between α
and {y : β // y ≠ x}≠ x}
.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.optionSubtype_apply_apply
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : { e // ↑e none = x })
(a : α)
(h : ↑↑e (some a) ≠ x)
:
↑(↑(Equiv.optionSubtype x) e) a = { val := ↑↑e (some a), property := h }
@[simp]
theorem
Equiv.coe_optionSubtype_apply_apply
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : { e // ↑e none = x })
(a : α)
:
↑(↑(↑(Equiv.optionSubtype x) e) a) = ↑↑e (some a)
@[simp]
theorem
Equiv.optionSubtype_apply_symm_apply
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : { e // ↑e none = x })
(b : { y // y ≠ x })
:
some (↑(Equiv.symm (↑(Equiv.optionSubtype x) e)) b) = ↑(Equiv.symm ↑e) ↑b
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_coe
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : α ≃ { y // y ≠ x })
(a : α)
:
↑↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) (some a) = ↑(↑e a)
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_some
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : α ≃ { y // y ≠ x })
(a : α)
:
↑↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) (some a) = ↑(↑e a)
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_none
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : α ≃ { y // y ≠ x })
:
↑↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) none = x
@[simp]
theorem
Equiv.optionSubtype_symm_apply_symm_apply
{α : Type u_2}
{β : Type u_1}
[inst : DecidableEq β]
(x : β)
(e : α ≃ { y // y ≠ x })
(b : { y // y ≠ x })
:
↑(Equiv.symm ↑(↑(Equiv.symm (Equiv.optionSubtype x)) e)) ↑b = some (↑(Equiv.symm e) b)