map_incl_lt_iff_lt_top — Mathlib

English

For a submodule N' of N, the inequality involving map along N.incl and comparison with top is equivalent to a similar inequality on N'.

Русский

Для подмодуля N' подмодуля N неравенство через отображение по N.incl эквивалентно аналогичному неравенству для N'.

LaTeX

$$$\forall N',\; N'.map (N.incl) < N \Leftrightarrow N' < \top$$$

Lean4

@[simp]
theorem map_incl_lt_iff_lt_top {N' : LieSubmodule R L N} : N'.map (LieSubmodule.incl N) < N ↔ N' < ⊤ :=
  by
  convert (LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt
  simp

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