lowerClosure_le — Mathlib

English

Let α be a preorder and s ⊆ α, t a lower set. Then the lower closure of s is contained in t if and only if s ⊆ t.

Русский

Пусть α — множество с предоридованием, s ⊆ α, t — нижнее множество. Тогда замыкание снизу s содержится в t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$\mathrm{lowerClosure}(s) \le t \Leftrightarrow s \subseteq t$$$

Lean4

@[simp]
theorem lowerClosure_le {t : LowerSet α} : lowerClosure s ≤ t ↔ s ⊆ t :=
  ⟨fun h ↦ subset_lowerClosure.trans <| LowerSet.coe_subset_coe.2 h, fun h ↦ lowerClosure_min h t.lower⟩

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