le_iff_mem — Mathlib

English

If s ≤ t and t is closed, then the topological closure of s is contained in t: s.topologicalClosure ≤ t.

Русский

Если s ⊆ t и t замкнуто, то топологическое замыкание s содержится в t: s.topologicalClosure ≤ t.

LaTeX

$$$s.topologicalClosure \le t$ given $s \le t$ and IsClosed(t)$$$

Lean4

theorem le_iff_mem {x : A} {s : NonUnitalSubalgebra R A} (hs : IsClosed (s : Set A)) : elemental R x ≤ s ↔ x ∈ s :=
  ⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

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