not_finite — Mathlib

English

There is no type that is both finite and infinite.

Русский

Не существует типа, который был бы одновременно конечным и бесконечным.

LaTeX

$$$\\forall \\alpha, \\operatorname{Infinite}(\\alpha) \\land \\operatorname{Finite}(\\alpha) \\Rightarrow \\False.$$$

Lean4

/-- `Infinite α` is not `Finite` -/
theorem not_finite (α : Sort*) [Infinite α] [Finite α] : False :=
  @Infinite.not_finite α ‹_› ‹_›

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