mem_compl_of_ge

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.mem_compl_of_ge

English

If x ≤ y and x ∈ I^c, then y ∈ I^c.

Русский

Если x ≤ y и x не принадлежит I, тогда y не принадлежит I.

LaTeX

$$$ x \\le y \\Rightarrow x \\in I^c \\Rightarrow y \\in I^c $$$

Lean4

theorem mem_compl_of_ge {x y : P} : x ≤ y → x ∈ (I : Set P)ᶜ → y ∈ (I : Set P)ᶜ := fun h ↦ mt <| I.lower h

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

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

Разделы

Аффилиация

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