sInter_mul_subset — Mathlib

English

For a set of sets S and a fixed t, the intersection ⋂ S multiplied by t is contained in ⋂ s ∈ S, s * t.

Русский

Для множества множеств S и фиксированного t, ⋂ S · t ⊆ ⋂ s ∈ S, s · t.

LaTeX

$$$(S.sInter) * t \\subseteq \\bigcap_{s \\in S} (s * t)$$$

Lean4

@[to_additive]
theorem sInter_mul_subset (S : Set (Set α)) (t : Set α) : ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t :=
  image2_sInter_left_subset S t (fun a b => a * b)

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