inv_mem_Ioc_iff — Mathlib

English

In a commutative ordered monoid with inversion, a⁻¹ is in the half-open interval (c,d] iff a lies in (d⁻¹,c⁻¹].

Русский

В упорядоченной группе: a⁻¹ входит в интервал (c,d] тогда и только тогда, когда a принадлежит (d⁻¹,c⁻¹].

LaTeX

$$$a^{-1} \in \mathrm{Ioc}(c,d) \iff a \in \mathrm{Ioc}(d^{-1}, c^{-1})$$$

Lean4

@[to_additive]
theorem inv_mem_Ioc_iff : a⁻¹ ∈ Set.Ioc c d ↔ a ∈ Set.Ico d⁻¹ c⁻¹ :=
  and_comm.trans <| and_congr inv_le' lt_inv'

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