coe_mk' — Mathlib

English

The underlying set of mk' equals the carrier.

Русский

Множество, лежащее в mk', совпадает с носителем.

LaTeX

$$(mk'(carrier, zero_mem, add_mem, neg_mem, mul_mem_left, mul_mem_right) : Set R) = carrier$$

Lean4

@[simp]
theorem coe_mk' (carrier : Set R) (zero_mem add_mem neg_mem mul_mem_left mul_mem_right) :
    (mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right : Set R) = carrier :=
  Set.ext <| mem_mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right

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