mk_zero

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ico.mk_zero

English

If 0 ∈ Ico(0,1), then the canonical zero element ⟨0,h⟩ equals 0.

Русский

Если 0 ∈ Ico(0,1), то канонический элемент нуль ⟨0,h⟩ равен нулю.

LaTeX

$$$⟨0,h⟩ = 0$$$

Lean4

@[simp]
theorem mk_zero [Nontrivial R] (h : (0 : R) ∈ Ico (0 : R) 1) : (⟨0, h⟩ : Ico (0 : R) 1) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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