mk_range_inl — Mathlib

English

The cardinality of the range of Sum.inl equals the lift of the cardinality of α: |range Sum.inl| = lift |α|.

Русский

Кардинал образа Sum.inl равен подъёму кардинала α: |range Sum.inl| = lift |α|.

LaTeX

$$$|\\operatorname{range}(\\mathrm{Sum}.inl)| = \\text{lift}(|\\alpha|)$$$

Lean4

@[simp]
theorem mk_range_inl {α : Type u} {β : Type v} : #(range (@Sum.inl α β)) = lift.{v} #α := by
  rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]

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