antitone_principal

Mathlib.Order.PFilter

URI: https://scilib.ai/kg/mathlib#Order.PFilter.antitone_principal

English

The principal map is order-reversing: if p ≤ q then principal(q) ≤ principal(p).

Русский

Карта principal отдает порядок вверх: если p ≤ q, то principal(q) ≤ principal(p).

LaTeX

$$$$ p \\le q \\implies \\operatorname{principal}(q) \\le \\operatorname{principal}(p). $$$$

Lean4

theorem antitone_principal : Antitone (principal : P → PFilter P) := fun _ _ => principal_le_principal_iff.2

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

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

Разделы

Аффилиация

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