zero_eq_top — Mathlib

English

The bottom element is equal to the top exactly when n = 1: (0 : Fin n) = ⊤ ⇔ n = 1.

Русский

Нижний элемент равен верхнему тогда и только тогда, когда n = 1: (0 : Fin n) = ⊤ ⇔ n = 1.

LaTeX

$$$(0 : \mathrm{Fin}(n)) = \top \;\Longleftrightarrow\; n = 1$$$

Lean4

@[simp]
theorem zero_eq_top {n : ℕ} [NeZero n] : (0 : Fin n) = ⊤ ↔ n = 1 := by
  rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one, le_one_iff_eq_zero_or_eq_one,
    or_iff_right (NeZero.ne n)]

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