instCanLiftENatOfENatLeAleph0 — Mathlib

English

There exists a CanLift structure from Cardinal to ℕ∞ such that the inequality ≤ with aleph0 corresponds to ENat ordering; this formalizes that ENat values are at most aleph0 in cardinal terms.

Русский

Существует структура CanLift между Cardinal и ℕ∞, которая обеспечивает, что отношение ≤ с пределом aleph0 соответствует порядку ENat; формализует, что значения ENat не превосходят aleph0 в терминах кардиналов.

LaTeX

$$CanLift Cardinal \mathbb{N}_\infty Cardinal.ofENat (≤ \aleph0)$$

Lean4

instance : CanLift Cardinal ℕ∞ (↑) (· ≤ ℵ₀) where prf x := (Set.ext_iff.1 range_ofENat x).2

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