mem_iSup_prop — Mathlib

English

For a directed iSup of monoids, x is in the iSup if and only if either x = 1 or there exists some i with x ∈ S_i.

Русский

Для iSup над моноидами: x принадлежит iSup ⇔ x = 1 или существует i такое, что x ∈ S_i.

LaTeX

$$$x \in iSup S \iff (x = 1) \lor (\exists i, x \in S_i)$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_iSup_prop {p : Prop} {S : p → Submonoid M} {x : M} : x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h := by
  by_cases h : p <;> simp +contextual [h]

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