biUnionIndex_le — Mathlib

English

If J is in the BiUnion of πi, then J lies below the associated BiUnionIndex: J ≤ π.biUnionIndex πi J.

Русский

Если J принадлежит BiUnion(πi), то J лежит ниже соответствующего BiUnionIndex: J ≤ π.biUnionIndex πi J.

LaTeX

$$$ J \\in π.biUnion π_i \\Rightarrow J \\le π.biUnionIndex π_i J $$$

Lean4

theorem biUnionIndex_le (πi : ∀ J, Prepartition J) (J : Box ι) : π.biUnionIndex πi J ≤ I :=
  by
  by_cases hJ : J ∈ π.biUnion πi
  · exact π.le_of_mem (π.biUnionIndex_mem hJ)
  · rw [biUnionIndex, dif_neg hJ]

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