Locale.PT.isOpen_iff

theorem Locale.PT.isOpen_iff : ∀ (L : Type u_1) [inst : CompleteLattice L] (U : Set (Locale.PT L)), IsOpen U ↔ ∃ u, {x | x u} = U

This theorem provides a characterization of when a subset of the space of points of a complete lattice is open. It states that for any complete lattice `L`, and any set `U` of points in `L`, `U` is open if and only if there exists an element `u` such that `U` is exactly the set of points `x` where `x u` holds. This connects the concept of topological 'openness' with the existence of a specific condition that every element in the set satisfies.

More concisely: A subset of a complete lattice is open if and only if it is exactly the set of points satisfying a certain condition with respect to some element in the lattice.