ext

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

If the underlying sets of I and J are disjoint, then I ≠ J.

Русский

Если множества I и J, лежащие в основе коробок, непересекаются, то I ≠ J.

LaTeX

$$$ Disjoint I.toSet J.toSet \\Rightarrow I \\neq J $$$

Lean4

@[ext]
theorem ext (H : ∀ x, x ∈ I ↔ x ∈ J) : I = J :=
  injective_coe <| Set.ext H

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

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

Разделы

Аффилиация

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