ClosedUnder — Mathlib

English

ClosedUnder expresses closure of a set under a given function symbol.

Русский

Подмножество s структуры M замкнуто относительно функции f арности n, если для любого n-кортежа x элементов s значение f(x) принадлежит s.

LaTeX

$$ClosedUnder L f s := ∀ x : Fin n → M, (∀ i : Fin n, x i ∈ s) → funMap f x ∈ s$$

Lean4

/-- Indicates that a set in a given structure is a closed under a function symbol. -/
def ClosedUnder : Prop :=
  ∀ x : Fin n → M, (∀ i : Fin n, x i ∈ s) → funMap f x ∈ s

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