mk'_eq_coe

Mathlib.Analysis.BoxIntegral.Box.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.mk'_eq_coe

← MathLib Explorer

English

mk' l u equals I iff l equals I.lower and u equals I.upper.

Русский

mk' l u равно I тогда, когда l = I.lower и u = I.upper.

LaTeX

$$$mk'(l,u) = I \iff (l = I.lower) \land (u = I.upper)$$$

Lean4

@[simp]
theorem mk'_eq_coe {l u : ι → ℝ} : mk' l u = I ↔ l = I.lower ∧ u = I.upper :=
  by
  obtain ⟨lI, uI, hI⟩ := I; rw [mk']; split_ifs with h
  · simp
  · suffices l = lI → u ≠ uI by simpa
    rintro rfl rfl
    exact h hI

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

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

Разделы

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

Аффилиация

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