Iic_ne_Iic

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.Iic_ne_Iic

English

Elements are equal if and only if their principal lower sets are equal: Iic a ≠ Iic b iff a ≠ b.

Русский

Элементы равны тогда и только тогда, когда их порожденные нижние множества различны: Iic a ≠ Iic b ⇔ a ≠ b.

LaTeX

$$Iff (Ne (LowerSet.Iic a) (LowerSet.Iic b)) (Ne a b)$$

Lean4

theorem Iic_ne_Iic : Iic a ≠ Iic b ↔ a ≠ b :=
  Iic_inj.not

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

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

Разделы

Аффилиация

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