iInter₂_congr — Mathlib

English

If ∀ i j, s(i) j = t(i) j, then ⋂_i ⋂_j s(i) j = ⋂_i ⋂_j t(i) j.

Русский

Если ∀ i, ∀ j, s(i) j = t(i) j, то ⋂_i ⋂_j s(i) j = ⋂_i ⋂_j t(i) j.

LaTeX

$$$$ \\forall i, \\forall j,\\ s(i,j) = t(i,j) \\Rightarrow \\bigcap_{i} \\bigcap_{j} s(i,j) = \\bigcap_{i} \\bigcap_{j} t(i,j) $$$$

Lean4

theorem iInter₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) : ⋂ (i) (j), s i j = ⋂ (i) (j), t i j :=
  iInter_congr fun i => iInter_congr <| h i

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