preimage_cast_Ioi — Mathlib

English

Let m, n be natural numbers with m = n, and i ∈ Fin n. Then the preimage of the interval Ioi i under Fin.cast h is Ioi (i.cast h.symm).

Русский

Пусть m, n — натуральные числа и m = n, и пусть i ∈ Fin n. Тогда прообраз интервала Ioi i по отображению Fin.cast h равен Ioi (i.cast h.symm).

LaTeX

$$$ \operatorname{Set.preimage}(\operatorname{Fin.cast} h)\, (\operatorname{Set.Ioi} i) = \operatorname{Ioi}(i.cast\, h.symm) $$$

Lean4

@[simp]
theorem preimage_cast_Ioi (h : m = n) (i : Fin n) : .cast h ⁻¹' Ioi i = Ioi (i.cast h.symm) :=
  rfl

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