map_eq_top_iff — Mathlib

English

There exists an order isomorphism between Submodule R M and Submodule R₂ M₂ when there is a bijective semilinear map f: the isomorphism is given by map f with inverse comap f.

Русский

Существуют взаимно однозначные отображения решетки подмодулов при биективном полуприводе f: отображение между подмодулями задается через map f и имеет обратное comap f.

LaTeX

$$$\exists \phi:\, Submodule\; R\; M \cong_o Submodule\; R_2\; M_2,\ phi(p) = map\ f\, p,\ phi^{-1}(q) = comap\ f\ q$$$

Lean4

@[simp]
protected theorem map_eq_top_iff : p.map e = ⊤ ↔ p = ⊤ :=
  map_eq_top_iff (orderIsoMapComap e)

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