inv_le_inv_iff

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.inv_le_inv_iff

← MathLib Explorer

English

For filters f and g, f^{-1} ≤ g^{-1} if and only if f ≤ g.

Русский

Для фильтров f и g: f^{-1} ≤ g^{-1} тогда и только тогда, когда f ≤ g.

LaTeX

$$$$ f^{-1} \le g^{-1} \iff f \le g. $$$$

Lean4

@[to_additive (attr := simp)]
protected theorem inv_le_inv_iff : f⁻¹ ≤ g⁻¹ ↔ f ≤ g :=
  ⟨fun h => inv_inv f ▸ inv_inv g ▸ Filter.inv_le_inv h, Filter.inv_le_inv⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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