Icc_eq

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#CovBy.Icc_eq

English

If a ⋖ b, then Icc(a,b) = {a, b}.

Русский

Если a ⋖ b, то Icc(a,b) = {a, b}.

LaTeX

$$Icc(a,b) = \{ a, b \}$$

Lean4

theorem Icc_eq (h : a ⋖ b) : Icc a b = { a, b } :=
  h.wcovBy.Icc_eq

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

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

Разделы

Аффилиация

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