inv_anti_mono — Mathlib

English

If I ≤ 1, then I ≤ I I^{-1}.

Русский

Если I ≤ 1, то I ≤ I I^{-1}.

LaTeX

$$$$I \le 1 \Rightarrow I \le I \cdot I^{-1}.$$$$

Lean4

theorem inv_anti_mono (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) : J⁻¹ ≤ I⁻¹ := by
  -- Porting note: in Lean3, introducing `x` would just give `x ∈ J⁻¹ → x ∈ I⁻¹`, but
    --  in Lean4, it goes all the way down to the subtypes

  intro x
  simp only [val_eq_coe, mem_coe, mem_inv_iff hJ, mem_inv_iff hI]
  exact fun h y hy => h y (hIJ hy)

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