English
A lifted sigma-congruence: mk_sigma_congr_lift states that if e is an equivalence between index types and the fibers have matching lifted cardinalities, then the lifted sigma-types have equal cardinalities.
Русский
Подъем сигма-конгруэнтности: если есть эквивелентность между индексами и объёмы фибр удовлетворяют условию, то поднятые сигма-типы имеют одинаковые кардиналы.
LaTeX
$$$\forall {\iota \; \iota',\; f\; g},\; (e : \iota \simeq \iota')\; (\forall i, \lift(|f(i)|) = \lift(|g(e(i))|)) \Rightarrow \lift|\Sigma i, f i| = \lift|\Sigma i, g i|$$$
Lean4
theorem mk_sigma_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι')
(h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) : lift.{max v' w'} #(Σ i, f i) = lift.{max v w} #(Σ i, g i) :=
Cardinal.lift_mk_eq'.2 ⟨.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩
