div_iInter₂_subset — Mathlib

English

Division distributes over a two-parameter intersction on the right: (s / ⋂ i (j), t i j) ⊆ ⋂ i (j), s / t i j.

Русский

Деление над двойным пересечением справа: (s / ⋂ i j, t(i,j)) ⊆ ⋂ i j, s / t(i,j).

LaTeX

$$$$ s / \bigcap_i \bigcap_j t(i,j) \subseteq \bigcap_i \bigcap_j (s / t(i,j)) $$$$

Lean4

@[to_additive]
theorem div_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s / t i j :=
  image2_iInter₂_subset_right ..

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