instCanLiftSetCoeAndMemOfNatForallForallForallForallHMul

English

There is a canonical way to turn a subset s ⊆ M with 1 ∈ s and closed under multiplication into a Submonoid of M; this provides a lifting from Sets to Submonoid.

Русский

Существует канонический способ превратить подмножество s ⊆ M, содержащее 1 и замкнутое относительно умножения, в подмономод M; это обеспечивает переход сверху Sets к Submonoid.

LaTeX

$$$$ \\text{If } 1\\in s \\text{ and } (\\forall x,y\\in s, xy\\in s), \\; s \\text{ is a Submonoid of } M $$$$

Lean4

@[to_additive]
instance (priority := 100) : CanLift (Set M) (Submonoid M) (↑) (fun s ↦ 1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s)
    where prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2 }, rfl⟩

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