iUnion_congr_Prop — Mathlib

English

If p ↔ q and f₁, f₂ correspond via pq, then the unions are equal: ⋃ f₁ = ⋃ f₂.

Русский

Если p и q эквивалютны и соответствия f₁ и f₂ согласованы через эквивалентность pq, то объединения равны: ⋃ f₁ = ⋃ f₂.

LaTeX

$$$iUnion f_1 = iUnion f_2$$$

Lean4

@[congr]
theorem iUnion_congr_Prop {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) :
    iUnion f₁ = iUnion f₂ :=
  iSup_congr_Prop pq f

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