eq_of_le

Mathlib.Analysis.BoxIntegral.Partition.Basic

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

English

If J1 and J2 are in π and J1 ≤ J2 then J1 = J2.

Русский

Если J1, J2 ∈ π и J1 ≤ J2, то J1 = J2.

LaTeX

$$$J_1 = J_2$$$

Lean4

theorem eq_of_le (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (hle : J₁ ≤ J₂) : J₁ = J₂ :=
  π.eq_of_le_of_le h₁ h₂ le_rfl hle

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

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

Разделы

Аффилиация

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