isLeast_iff_eq

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsLeast.isLeast_iff_eq

English

If ha is IsGLB s a, hb is IsLUB s b, hab is b ≤ a, and x,y ∈ s, then x ≤ y.

Русский

Пусть ha — IsGLB s a, hb — IsLUB s b, hab: b ≤ a, и x,y ∈ s, тогда x ≤ y.

LaTeX

$$$\text{IsGLB}(s,a) \rightarrow IsLUB(s,b) \rightarrow b \le a \rightarrow x \in s \rightarrow y \in s \rightarrow x \le y$$$

Lean4

theorem isLeast_iff_eq (Ha : IsLeast s a) : IsLeast s b ↔ a = b :=
  Iff.intro Ha.unique fun h => h ▸ Ha

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

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

Разделы

Аффилиация

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