subset_piiUnionInter — Mathlib

English

If i ∈ S, then every set in π i is contained in piiUnionInter π S. This makes intuitive sense: the construction with a singleton index i includes at least the i-th family.

Русский

Если i ∈ S, то каждый элемент π i содержится в piiUnionInter π S.

LaTeX

$$$\text{If } hiS: i \in S,\ \pi i \subseteq piiUnionInter(\pi,S).$$$

Lean4

theorem subset_piiUnionInter {π : ι → Set (Set α)} {S : Set ι} {i : ι} (his : i ∈ S) : π i ⊆ piiUnionInter π S :=
  by
  have h_ss : { i } ⊆ S := by
    intro j hj
    rw [mem_singleton_iff] at hj
    rwa [hj]
  refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)
  rw [piiUnionInter_singleton]
  exact subset_union_left

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