toENatAux_gc — Mathlib

English

The embedding of ENat into Cardinal and the projection to ENat form a Galois connection.

Русский

Встраивание ENat в кардиналы и проекция в ENat образуют гало-сициальное сопряжение.

LaTeX

$$$\\mathrm{GaloisConnection}(\\uparrow,\\operatorname{toENat})$$$

Lean4

theorem toENatAux_gc : GaloisConnection (↑) toENatAux := fun n x ↦ by
  cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

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