toENat — Mathlib

English

toENat acts as a canonical projection from Cardinal to ENat, extending the nat-casts.

Русский

toENat выступает в качестве канонической проекции кардиналов на ENat, расширяющей преобразование натуральных чисел.

LaTeX

$$$\\forall x \\in \\mathrm{Cardinal},\\; \\operatorname{toENat}(x) = \\operatorname{toENatAux}(x)$$$

Lean4

/-- Projection from cardinals to `ℕ∞`. Sends all infinite cardinals to `⊤`.

We define this function as a bundled monotone ring homomorphism. -/
noncomputable def toENat : Cardinal.{u} →+*o ℕ∞
    where
  toFun := toENatAux
  map_one' := toENatAux_nat 1
  map_mul' x
    y := by
    wlog hle : x ≤ y; · rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
    cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]
    | inr hy =>
      rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (one_le_iff_ne_zero.2 hx) hy
  map_add' x
    y := by
    wlog hle : x ≤ y; · rw [add_comm, this y x (le_of_not_ge hle), add_comm]
    cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]
    | inr hy =>
      simp only [toENatAux_eq_top hy, add_top]
      exact toENatAux_eq_top <| le_add_left hy
  map_zero' := toENatAux_zero
  monotone' := toENatAux_gc.monotone_u

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