mem_biUnion

Mathlib.Analysis.BoxIntegral.Partition.Basic

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

English

J belongs to the biUnion of π with πi iff there exists J′ ∈ π such that J ∈ πi J′.

Русский

J принадлежит biUnion π при выборе πi тогда, когда существует J′ ∈ π, такое что J ∈ πi J′.

LaTeX

$$J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'$$

Lean4

@[simp]
theorem mem_biUnion : J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J' := by simp [biUnion]

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

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

Разделы

Аффилиация

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