isExtrFilter_dual_iff

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#isExtrFilter_dual_iff

English

IsExtrFilter (toDual ∘ f) l a is equivalent to IsExtrFilter f l a.

Русский

IsExtrFilter (toDual ∘ f) l a эквивалентен IsExtrFilter f l a.

LaTeX

$$$IsExtrFilter (toDual \circ f) l a \leftrightarrow IsExtrFilter f l a$$$

Lean4

theorem isExtrFilter_dual_iff : IsExtrFilter (toDual ∘ f) l a ↔ IsExtrFilter f l a :=
  or_comm

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

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

Разделы

Аффилиация

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