dual_inv_le — Mathlib

English

The inverse of the dual of I is contained in I: (dual_{A,K}(I))^{-1} ⊆ I.

Русский

Обратная стороны двойственной к I содержится в I: (dual_{A,K}(I))^{-1} ⊆ I.

LaTeX

$$$(\mathrm{dual}_{A,K}(I))^{-1} \leq I$$$

Lean4

theorem dual_inv_le : (dual A K I)⁻¹ ≤ I := by
  by_cases hI : I = 0; · simp [hI]
  convert mul_right_mono ((dual A K I)⁻¹) (mul_left_mono I (inv_le_dual A K I)) using 1
  · simp only [mul_inv_cancel₀ hI, one_mul]
  · simp only [mul_inv_cancel₀ (dual_ne_zero A K (hI := hI)), mul_assoc, mul_one]

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