closure_le — Mathlib

English

The closure operation is order-preserving in the sense that closure(s) ≤ L iff s ⊆ L for any Boolean subalgebra L.

Русский

Операция замыкания монотонна относительно порядка: closure(s) ≤ L эквивалентно s ⊆ L для любого булева подполья L.

LaTeX

$$$\\mathrm{closure}(s) \\le L \\iff s \\subseteq L$$$

Lean4

@[simp]
theorem closure_le : closure s ≤ L ↔ s ⊆ L :=
  ⟨subset_closure.trans, fun h ↦ sInf_le h⟩

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