mk_le_mk — Mathlib

English

Let S and T be submonoids of G with appropriate inverse-closure hypotheses. Then the corresponding subgroups satisfy H_S ≤ H_T if and only if S ≤ T.

Русский

Пусть S и T — подмонойды G, удовлетворяющие подходящим условиям обратимости. Тогда соответствующие подгруппы удовлетворяют H_S ≤ H_T тогда и только тогда, когда S ≤ T.

LaTeX

$$$H_S \\le H_T \\iff S \\le T$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Submonoid G} (h_inv) (h_inv') : mk s h_inv ≤ mk t h_inv' ↔ s ≤ t :=
  Iff.rfl

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