piiUnionInter_mono_left — Mathlib

English

If π ≤ π' pointwise, then piiUnionInter π S ⊆ piiUnionInter π' S for any S. Monotonicity with respect to the family coordinate.

Русский

Если для каждого i выполняется π(i) ⊆ π'(i), тогда piiUnionInter(π,S) ⊆ piiUnionInter(π',S). Монотоничность по координатам семейства.

LaTeX

$$$\forall i, \pi i \subseteq \pi' i \Rightarrow \forall S, \ piiUnionInter(π,S) \subseteq piiUnionInter(π',S)$$$

Lean4

theorem piiUnionInter_mono_left {π π' : ι → Set (Set α)} (h_le : ∀ i, π i ⊆ π' i) (S : Set ι) :
    piiUnionInter π S ⊆ piiUnionInter π' S := fun _ ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩ =>
  ⟨t, ht_mem, ft, fun x hxt => h_le x (hft_mem_pi x hxt), h_eq⟩

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