enat_gc — Mathlib

English

The coercion of ENat into Cardinal and the projection to ENat form a Galois coinsertion.

Русский

Приведение ENat к Cardinal и проекция обратно в ENat образуют гало-коинсерцию.

LaTeX

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

Lean4

/-- The coercion `Cardinal.ofENat` and the projection `Cardinal.toENat` form a Galois connection.
See also `Cardinal.gciENat`. -/
theorem enat_gc : GaloisConnection (↑) toENat :=
  toENatAux_gc

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