eq_of_mem_uIcc_of_mem_uIcc

Mathlib.Order.Interval.Set.UnorderedInterval

URI: https://scilib.ai/kg/mathlib#Set.eq_of_mem_uIcc_of_mem_uIcc

← MathLib Explorer

English

In a distributive lattice, if a ∈ [[b, c]] and b ∈ [[a, c]], then a = b.

Русский

В распределительной решётке, если a ∈ [[b,c]] и b ∈ [[a,c]], то a = b.

LaTeX

$$$ (ha:\\ a \\in [[b,c]]) \\land (hb:\\ b \\in [[a,c]]) \\Rightarrow a = b $$$

Lean4

theorem eq_of_mem_uIcc_of_mem_uIcc (ha : a ∈ [[b, c]]) (hb : b ∈ [[a, c]]) : a = b :=
  eq_of_inf_eq_sup_eq (inf_congr_right ha.1 hb.1) <| sup_congr_right ha.2 hb.2

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

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

Разделы

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

Аффилиация

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