mrange_subtype — Mathlib

English

For a submonoid s of M, mrange s.subtype = s; the range of the subtype embedding equals the submonoid itself.

Русский

Для подмножества s подмножества M, образ подтипа совпадает с самой подмономой.

LaTeX

$$$ \operatorname{mrange}(s.\text{subtype}) = s $$$

Lean4

@[to_additive (attr := simp)]
theorem mrange_subtype (s : Submonoid M) : mrange s.subtype = s :=
  SetLike.coe_injective <| (coe_mrange _).trans <| Subtype.range_coe

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