mem_iUnion — Mathlib

English

For any point x, x belongs to the iUnion if and only if there exists a box J in π that contains x.

Русский

Для любой точки x выполняется: x принадлежит iUnion тогда и только тогда, когда существует коробка J в π, содержащая x.

LaTeX

$$$ x \\in \\pi.iUnion \\iff \\exists J \\in \\pi,\\; x \\in J $$$

Lean4

@[simp]
theorem mem_iUnion : x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J :=
  by
  convert Set.mem_iUnion₂
  rw [Box.mem_coe, mem_toPrepartition, exists_prop]

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