cast_toNat_eq_iff_lt_aleph0 — Mathlib

English

toNat c = c iff c < aleph0.

Русский

toNat c = c тогда и только тогда, когда c < aleph0.

LaTeX

$$toNat c = c \iff c < \aleph_0$$

Lean4

theorem cast_toNat_eq_iff_lt_aleph0 {c : Cardinal} : (toNat c) = c ↔ c < ℵ₀ :=
  by
  constructor
  · intro h; by_contra h'; rw [not_lt] at h'
    rw [toNat_apply_of_aleph0_le h'] at h; rw [← h] at h'
    absurd h'; rw [not_le]; exact nat_lt_aleph0 0
  · exact fun h ↦ (Cardinal.cast_toNat_of_lt_aleph0 h)

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