inv_le_self

Mathlib.Order.Filter.Pointwise

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

English

For any filter f, f^{-1} ≤ f implies f^{-1} = f.

Русский

Для любого фильтра f, если f^{-1} ≤ f, то f^{-1} = f.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem inv_le_self : f⁻¹ ≤ f ↔ f⁻¹ = f :=
  ⟨fun h => h.antisymm <| inv_le_iff_le_inv.1 h, Eq.le⟩

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

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

Разделы

Аффилиация

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