exists_isNilRegular — Mathlib

English

In a broader setting with IsDomain or Infinite R, there exists x with IsNilRegular φ x under appropriate cardinal conditions.

Русский

В более общем контексте при подходящих кардинальных условиях существует x с IsNilRegular φ x.

LaTeX

$$∃ x : L, IsNilRegular φ x$$

Lean4

theorem exists_isNilRegular [Infinite R] : ∃ x : L, IsNilRegular φ x :=
  by
  apply exists_isNilRegular_of_finrank_le_card
  exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

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