biInter_mono — Mathlib

English

If s ⊆ s' and ∀ x ∈ s, t x ⊆ t' x, then ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t' x.

Русский

Если s ⊆ s' и для всех x ∈ s выполнено t x ⊆ t' x, тогда ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t' x.

LaTeX

$$$$ s \\subseteq s' \\Rightarrow \\bigcap_{x \\in s} t(x) \\subseteq \\bigcap_{x \\in s'} t'(x). $$$$

Lean4

theorem biInter_mono {s s' : Set α} {t t' : α → Set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) :
    ⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x :=
  (biInter_subset_biInter_left hs).trans <| iInter₂_mono h

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