piiUnionInter_mono_right — Mathlib

English

If S ⊆ T, then piiUnionInter π S ⊆ piiUnionInter π T. The construction enlarges the index set, so the resulting family only grows.

Русский

Если S ⊆ T, то piiUnionInter π S ⊆ piiUnionInter π T. Набор множества растёт по мере увеличения индексов.

LaTeX

$$$S \subseteq T \Rightarrow piiUnionInter(\pi) S \subseteq piiUnionInter(\pi) T$$$

Lean4

theorem piiUnionInter_mono_right {π : ι → Set (Set α)} {S T : Set ι} (hST : S ⊆ T) :
    piiUnionInter π S ⊆ piiUnionInter π T := fun _ ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩ =>
  ⟨t, ht_mem.trans hST, ft, hft_mem_pi, h_eq⟩

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