English
Let a ∈ α. If the subtype { b ∈ α | b ≠ a } is finite, then α is finite; equivalently, |α| = 1 + |{ b ∈ α | b ≠ a }|.
Русский
Пусть a ∈ α. Если подтип { b ∈ α | b ≠ a } конечен, то α также конечен; эквивалентно чему-то вроде |α| = 1 + |{ b ∈ α | b ≠ a }|.
LaTeX
$$$$|\\alpha| = 1 + \\left|\\{ b \\in \\alpha \\mid b \\neq a \\} \\right|.$$$$
Lean4
/-- If the subtype of all-but-one elements is a `Fintype` then the type itself is a `Fintype`. -/
def fintypeOfFintypeNe (a : α) (_ : Fintype { b // b ≠ a }) : Fintype α :=
Fintype.ofBijective (Sum.elim ((↑) : { b // b = a } → α) ((↑) : { b // b ≠ a } → α)) <| by
classical exact (Equiv.sumCompl (· = a)).bijective
