div_sInter_subset — Mathlib

English

For a fixed set s and a family T of sets, s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t.

Русский

Для фиксированного множества s и семейства T множество s / ⋂₀ T содержится в ⋂_{t∈T} (s / t).

LaTeX

$$$$ s / \bigcap_0 T \subseteq \bigcap_{t \in T} (s / t) $$$$

Lean4

@[to_additive]
theorem div_sInter_subset (s : Set α) (T : Set (Set α)) : s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t :=
  image2_sInter_subset_right ..

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