mem_closed_of_isRelational — Mathlib

English

If the language L is relational, then every subset s is closed under the closure operator.

Русский

Если язык L является релальным, то любое подмножество s замкнуто относительно оператора замыкания.

LaTeX

$$$$ s \in (\operatorname{closure}_L).closed, $$$$

Lean4

theorem mem_closed_of_isRelational [L.IsRelational] (s : Set M) : s ∈ (closure L).closed :=
  (mem_closed_iff s).2 isEmptyElim

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