optionSubtype — Mathlib

English

For x ∈ β and e : { e : Option α ≃ β // e none = x }, the forward map sends a ∈ α to ⟨(e : Option α ≃ β) a, h⟩, where h is the witness e none = x.

Русский

Пусть x ∈ β и e : { e : Option α ≃ β // e none = x }. Прямое отображение отправляет a ∈ α в ⟨(e : Option α ≃ β) a, h⟩, где h — свидетельство e none = x.

LaTeX

$$$\mathrm{optionSubtype}\ x\ e\; a = \langle (e : \mathrm{Option} \alpha \simeq \beta) a, h \rangle.$$$

Lean4

/-- Equivalences between `Option α` and `β` that send `none` to `x` are equivalent to
equivalences between `α` and `{y : β // y ≠ x}`. -/
def optionSubtype [DecidableEq β] (x : β) : { e : Option α ≃ β // e none = x } ≃ (α ≃ { y : β // y ≠ x })
    where
  toFun
    e :=
    { toFun := fun a => ⟨(e : Option α ≃ β) a, ((EquivLike.injective _).ne_iff' e.property).2 (some_ne_none _)⟩,
      invFun := fun b =>
        get _
          (ne_none_iff_isSome.1
            (((EquivLike.injective _).ne_iff' ((apply_eq_iff_eq_symm_apply _).1 e.property).symm).2 b.property)),
      left_inv := fun a => by
        rw [← some_inj, some_get]
        exact symm_apply_apply (e : Option α ≃ β) a,
      right_inv := fun b => by
        ext
        simp }
  invFun
    e :=
    ⟨{ toFun := fun a => casesOn' a x (Subtype.val ∘ e), invFun := fun b => if h : b = x then none else e.symm ⟨b, h⟩,
        left_inv := fun a => by
          cases a with
          | none => simp
          | some
            a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta, symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property,
        right_inv := fun b => by by_cases h : b = x <;> simp [h] },
      rfl⟩
  left_inv
    e := by
    ext a
    cases a
    · simpa using e.property.symm
    · simp
  right_inv
    e := by
    ext a
    rfl

Похожие утверждения