mk_le_mk — Mathlib

English

For s,t Subsemigroups and their corresponding mk constructions, mk s h ≤ mk t h' iff s ≤ t.

Русский

Для s,t Subsemigroup и соответствующих конструкторов mk, выполняется mk s h ≤ mk t h' тогда и только тогда, когда s ≤ t.

LaTeX

$$$$ mk\\,s\\,h\\_one \\le mk\\,t\\,h\\_one' \\iff s \\le t $$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Subsemigroup M} (h_one) (h_one') : mk s h_one ≤ mk t h_one' ↔ s ≤ t :=
  Iff.rfl

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