mk_sigma_congr — Mathlib

English

If e: ι ≃ ι' is an equivalence and (∀ i, |f i| = |g(e i)|), then |Σ i, f i| = |Σ i, g i|.

Русский

Если e: ι ≃ ι' является эквивалентностью и (∀ i, |f i| = |g(e i)|), то |Σ i, f i| = |Σ i, g i|.

LaTeX

$$$\forall (e : Equiv\, ι\, ι'),\; (\forall i, |f i| = |g (e i)|) \Rightarrow |\Sigma i, f i| = |\Sigma i, g i|$$$

Lean4

theorem mk_sigma_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ i, #(f i) = #(g (e i))) :
    #(Σ i, f i) = #(Σ i, g i) :=
  mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

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