ext

Mathlib.Analysis.BoxIntegral.Partition.Basic

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

English

Two prepartitions are equal if they have the same membership relation for all boxes.

Русский

Два предразбиения равны, если у них совпадает членство по всем коробкам.

LaTeX

$$$\pi_1 = \pi_2$$$

Lean4

@[ext]
theorem ext (h : ∀ J, J ∈ π₁ ↔ J ∈ π₂) : π₁ = π₂ :=
  injective_boxes <| Finset.ext h

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

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

Разделы

Аффилиация

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