closure_eq_of_le — Mathlib

English

Let S be a L-substructure of M with s ⊆ S and S ≤ closure_L(s). Then closure_L(s) = S.

Русский

Пусть S — подструктура L структуры M, удовлетворяющая s ⊆ S и S ≤ closure_L(s). Тогда closure_L(s) = S.

LaTeX

$$$$ s \subseteq S \land S \le \operatorname{closure}_L(s) \Rightarrow \operatorname{closure}_L(s) = S $$$$

Lean4

theorem closure_eq_of_le (h₁ : s ⊆ S) (h₂ : S ≤ closure L s) : closure L s = S :=
  (closure L).eq_of_le h₁ h₂

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