equiv_up — Mathlib

English

For any a ∈ α, the index given by the equivalence for ULift α at ULift.up a equals the index for a.

Русский

Для любого a ∈ α индекс, задаваемый эквивалентностью для ULift α при ULift.up a, равен индексу для a.

LaTeX

$$$ \\operatorname{equiv}_{(\\\\mathrm{ULift} \\\\alpha)}(\\\\mathrm{up}(a)) = \\operatorname{equiv}_{\\\\alpha}(a). $$$

Lean4

@[simp]
theorem equiv_up : equiv (ULift.up a) = equiv a :=
  rfl

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