withBotCoe_inj

Mathlib.Analysis.BoxIntegral.Box.Basic

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

← MathLib Explorer

English

Two boxes are equal iff their underlying sets coincide.

Русский

Две коробки равны тогда и только тогда, когда совпадают их подмножества.

LaTeX

$$$(I : Set (ι \to \mathbb{R})) = J \iff I = J$$$

Lean4

@[simp, norm_cast]
theorem withBotCoe_inj {I J : WithBot (Box ι)} : (I : Set (ι → ℝ)) = J ↔ I = J := by
  simp only [Subset.antisymm_iff, ← le_antisymm_iff, withBotCoe_subset_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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