mem_sup — Mathlib

English

Membership in the join of submonoids s and t is equivalent to existence of y in s and z in t with y z = x.

Русский

Членство в объединении подмоноидов s и t эквивалентно существованию y ∈ s и z ∈ t с y z = x.

LaTeX

$$$ x \\in s \\cup t \\quad\\Leftrightarrow\\quad \\exists y \\in s, \\exists z \\in t,\\ y z = x $$$

Lean4

@[to_additive]
theorem mem_sup {s t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := by
  simp only [sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists, Subtype.exists, exists_prop]

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