mk_range_inr — Mathlib

English

The cardinality of the range of Sum.inr equals the lift of the cardinality of β: |range Sum.inr| = lift |β|.

Русский

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

LaTeX

$$$|\\operatorname{range}(\\mathrm{Sum}.inr)| = \\text{lift}(|\\beta|)$$$

Lean4

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

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