OrderGenerates — Mathlib

English

T order-generates α if for every a ∈ α there exists a subset S ⊆ T such that a = kernel(S).

Русский

T порождает порядок, если для каждого a ∈ α существует подмножество S ⊆ T такое, что a = kernel(S).

LaTeX

$$$(\\forall a \\in \\alpha)\\; \\exists S \\subseteq T,\\ a = kernel(S).$$$

Lean4

/-- `T` order generates `α` if, for every `a` in `α`, there exists a subset of `T` such that `a` is
the `kernel` of `S`. -/
def OrderGenerates :=
  ∀ (a : α), ∃ (S : Set T), a = kernel S

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