nonempty_of_infiniteDimensionalOrder

English

Let α be a type with InfiniteDimensionalOrder. Then α is nonempty.

Русский

Пусть α обладает свойством бесконечно размерного порядка. Тогда α непуст.

LaTeX

$$$\forall \alpha\, (\text{InfiniteDimensionalOrder }\alpha) \Rightarrow \exists a:\alpha$$$

Lean4

/-- if `α` is infinite dimensional, then `α` is nonempty. -/
theorem nonempty_of_infiniteDimensionalOrder [InfiniteDimensionalOrder α] : Nonempty α :=
  ⟨LTSeries.withLength α 0 0⟩

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