_example — Mathlib

English

Alternative form: the closure of a set is the union of the singleton {1} with the subsemigroup closure of the set.

Русский

Альтернативная формулировка: замыкание множества есть объединение {1} с порождённым полусупмоном замыканием множества.

LaTeX

$$closure s = \\{1\\} ∪ (Subsemigroup.closure s)$$

Lean4

example {p : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, p x) (one : p 1)
    (mul : ∀ x y, p x → p y → p (x * y)) (x : M) : p x := by
  induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | one => exact one
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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