disjointOfUnion_subset_of_mem — Mathlib

English

With hC as above and hJ ⊆ C, for j ∈ J the sUnion of all blocks in hC.disjointOfUnion hJ j is contained in j.

Русский

Пусть hC и hJ как выше; для фиксированного j ∈ J выпуклая (объединение) всех блоков из hC.disjointOfUnion hJ j содержится в j.

LaTeX

$$$\bigcup\_{X \in h_C.disjointOfUnion(h_J, j)} X \subseteq j.$$$

Lean4

theorem disjointOfUnion_subset_of_mem (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
    ⋃₀ hC.disjointOfUnion hJ j ⊆ j :=
  (Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.2.1 j hj

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