coe_sup — Mathlib

English

Let N be a commutative monoid and H, K be submonoids of N. Then the underlying set of the join equals the product HK, i.e. ↑(H ⊔ K) = (H * K : Set N).

Русский

Пусть N — коммутативный моноид, H и K — подмоноиды N. Тогда множество, соответствующее объединению H и K, равно HK: ↑(H ⊔ K) = (H * K : Set N).

LaTeX

$$$\\uparrow(H \\sqcup K) = (H \\cdot K : \\mathrm{Set} N)$$$

Lean4

@[to_additive]
theorem coe_sup {N : Type*} [CommMonoid N] (H K : Submonoid N) : ↑(H ⊔ K) = (H * K : Set N) :=
  by
  ext x
  simp [mem_sup, Set.mem_mul]

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