iInter_congr_Prop — Mathlib

English

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

Русский

Если p и q эквивалентны и соответствия f₁, f₂ согласованы через pq, то пересечения равны: ⋂ f₁ = ⋂ f₂.

LaTeX

$$$iInter f_1 = iInter f_2$$$

Lean4

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

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