subset_of_mem_disjointOfUnion — Mathlib

English

If x is an element of hC.disjointOfUnion hJ j, then x is contained in j.

Русский

Пусть x ∈ hC.disjointOfUnion hJ j; тогда x ⊆ j.

LaTeX

$$$\forall X\,(X \in h_C.disjointOfUnion(h_J, j) \Rightarrow X \subseteq j).$$$

Lean4

theorem subset_of_mem_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) {x : Set α}
    (hx : x ∈ (hC.disjointOfUnion hJ) j) : x ⊆ j :=
  sUnion_subset_iff.mp (hC.disjointOfUnion_subset_of_mem hJ hj) x hx

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