consEquiv — Mathlib

English

There is a natural equivalence between the type of v ::ₘ m and the type Option m, i.e., (v ::ₘ m).ToType ≃ Option m.ToType.

Русский

Существует естественное эквивалентное отображение между типом v ::ₘ m и типом Option m, то есть (v ::ₘ m).ToType ≃ Option m.ToType.

LaTeX

$$$ {\alpha} \text{ and } {m} \text{ yield } (v \mathrel{::}_m m)^{\ToType} \simeq \mathrm{Option}(m^{\ToType}) $$$

Lean4

/-- `v ::ₘ m` is equivalent to `Option m` by mapping one `v` to `none` and everything else to `m`.
-/
def consEquiv {v : α} : v ::ₘ m ≃ Option m
    where
  toFun
    x :=
    if h : x.1 = v ∧ x.2.val = m.count v then none
    else
      some
        ⟨x.1,
          ⟨x.2, by
            by_cases hv : x.1 = v
            · simp only [hv, true_and] at h ⊢
              apply lt_of_le_of_ne (Nat.le_of_lt_add_one _) h
              convert x.2.2 using 1
              simp [hv]
            · convert x.2.2 using 1
              exact (count_cons_of_ne hv _).symm⟩⟩
  invFun x := x.elim ⟨v, ⟨m.count v, by simp⟩⟩ (fun x ↦ ⟨x.1, x.2.castLE (count_le_count_cons ..)⟩)
  left_inv := by
    rintro ⟨x, hx⟩
    dsimp only
    split
    · rename_i h
      obtain ⟨rfl, h2⟩ := h
      simp [← h2]
    · simp
  right_inv := by
    rintro (_ | x)
    · simp
    · simp only [Option.elim_some, Fin.coe_castLE, Fin.eta, Sigma.eta, dite_eq_ite, ite_eq_right_iff, reduceCtorEq,
        imp_false, not_and]
      rintro rfl
      exact x.2.2.ne

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