subsingleton_of_length_eq_zero — Mathlib

English

If s.length = 0, then the set {x | x ∈ s} is a Subsingleton.

Русский

Если длина s равна 0, то множество элементов s является s-подмножеством.

LaTeX

$$$s.length = 0 \\Rightarrow \\{x \\mid x \\in s\\} \\text{ is Subsingleton}$$$

Lean4

theorem subsingleton_of_length_eq_zero (hs : s.length = 0) : {x | x ∈ s}.Subsingleton :=
  by
  rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
  congr!
  exact finCongr (by rw [hs, zero_add]) |>.injective <| Subsingleton.elim (α := Fin 1) _ _

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