mem_closed_iff — Mathlib

English

A subset s is closed (i.e., belongs to the closed part of the closure) iff it is closed under every n-ary function symbol of the language L.

Русский

Подмножество s считается замкнутым (то есть принадлежит закрытому множеству замыкания) тогда и только тогда, когда оно замкнуто под всеми функцияциями языка L.

LaTeX

$$$$ s \in (\operatorname{closure}_L).closed \iff \forall {n}, \forall f : L.\mathrm{Functions}(n), \mathrm{ClosedUnder}(f, s). $$$$

Lean4

theorem mem_closed_iff (s : Set M) : s ∈ (closure L).closed ↔ ∀ {n}, ∀ f : L.Functions n, ClosedUnder f s :=
  by
  refine ⟨fun h n f => ?_, fun h => ?_⟩
  · rw [← h]
    exact Substructure.fun_mem _ _
  · have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure
    exact congr_arg _ h'

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