iInter_mono' — Mathlib

English

If for every j there exists i with s(i) ⊆ t(j), then ⋂_i s(i) ⊆ ⋂_j t(j).

Русский

Если для каждого j существует i, такой что s(i) ⊆ t(j), тогда ⋂_i s(i) ⊆ ⋂_j t(j).

LaTeX

$$$\forall j,\ exists i,\ s_i ⊆ t_j \Rightarrow \bigcap_i s_i \subseteq \bigcap_j t_j$$$

Lean4

theorem iInter_mono' {s : ι → Set α} {t : ι' → Set α} (h : ∀ j, ∃ i, s i ⊆ t j) : ⋂ i, s i ⊆ ⋂ j, t j :=
  Set.subset_iInter fun j =>
    let ⟨i, hi⟩ := h j
    iInter_subset_of_subset i hi

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