ClosureAntitone — Mathlib

English

ClosureAntitone strengthens Antitone by requiring that closure of each child-set is contained in its parent-set.

Русский

ClosureAntitone усиливает Antitone, требуя, чтобы замыкание A(a::l) было подмножество A(l).

LaTeX

$$$ \forall l: List\beta, \forall a: \beta, \mathrm{closure}(A(a::l)) \subseteq A(l). $$$

Lean4

/-- A useful strengthening of being antitone is to require that each set contains
the closure of each of its children. -/
def ClosureAntitone [TopologicalSpace α] : Prop :=
  ∀ l : List β, ∀ a : β, closure (A (a :: l)) ⊆ A l

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