mk_le_mk — Mathlib

English

The relation ≤ between AddSubmonoid S and S' is equivalent to the order between the corresponding Submodules defined by S and S'.

Русский

Относительная связь ≤ между AddSubmonoid S и S' эквивалентна порядку между соответствующими подмодулями, определяемыми S и S'.

LaTeX

$$$\\big( \\langle S, h \\rangle \\le \\langle S', h' \\rangle \\big) \\iff S \\le S'$$$

Lean4

@[simp]
theorem mk_le_mk {S S' : AddSubmonoid M} (h h') : (⟨S, h⟩ : Submodule R M) ≤ (⟨S', h'⟩ : Submodule R M) ↔ S ≤ S' :=
  Iff.rfl

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