mem_iUnion

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.mem_iUnion

English

A point x lies in π.iUnion iff there exists a box J in π with x ∈ J.

Русский

Точка x принадлежит π.iUnion тогда и только тогда, когда существует коробка J в π такая, что x ∈ J.

LaTeX

$$x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru