le_upperClosure — Mathlib

English

Let α be a preorder. For an upper set s and a subset t, s ≤ upperClosure(t) if and only if t ⊆ s.

Русский

Пусть α — множество с предоридованием. Для верхнего множества s и множества t, выполняется s ≤ upperClosure(t) тогда и только тогда, когда t ⊆ s.

LaTeX

$$$s \le \mathrm{upperClosure}(t) \iff t \subseteq s$$$

Lean4

@[simp]
theorem le_upperClosure {s : UpperSet α} : s ≤ upperClosure t ↔ t ⊆ s :=
  ⟨fun h ↦ subset_upperClosure.trans <| UpperSet.coe_subset_coe.2 h, fun h ↦ upperClosure_min h s.upper⟩

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