negOrderIso — Mathlib

English

Negation induces an order isomorphism on the lattice of submodules: S ≤ T iff -T ≤ -S.

Русский

Отрицание образует отображение-изоморфизм порядка на решетке подмодулей: S ≤ T тогда и только тогда, когда -T ≤ -S.

LaTeX

$$$\text{negOrderIso}: Submodule(R,M) \simeq_o Submodule(R,M)\ \text{with}\ \phi(S) = -S$$$

Lean4

/-- `Submodule.pointwiseNeg` as an order isomorphism. -/
def negOrderIso : Submodule R M ≃o Submodule R M
    where
  toEquiv := Equiv.neg _
  map_rel_iff' := @neg_le_neg _ _ _ _ _

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