Ici_ne_Ici

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_ne_Ici

English

Two principal upper sets are unequal if and only if their generating elements are different.

Русский

Два главных верхних множества различны тогда и только тогда, когда порождают их элементы различны.

LaTeX

$$$Ici(a) \neq Ici(b) \iff a \neq b$$$

Lean4

theorem Ici_ne_Ici : Ici a ≠ Ici b ↔ a ≠ b :=
  Ici_inj.not

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

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

Разделы

Аффилиация

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