English
Ring topologies on R form a complete lattice under the infimum operation, with ⊥ as discrete topology and ⊤ as indiscrete topology.
Русский
Топологии кольца на R образуют полную решетку относительно операции Inf, ⊥ — дискретная топология, ⊤ — недискретная топология.
LaTeX
$$RingTopology R forms a CompleteSemilatticeInf$$
Lean4
/-- Ring topologies on `R` form a complete lattice, with `⊥` the discrete topology and `⊤` the
indiscrete topology.
The infimum of a collection of ring topologies is the topology generated by all their open sets
(which is a ring topology).
The supremum of two ring topologies `s` and `t` is the infimum of the family of all ring topologies
contained in the intersection of `s` and `t`. -/
instance : CompleteSemilatticeInf (RingTopology R)
where
sInf := def_sInf
sInf_le := fun _ a haS => sInf_le (α := TopologicalSpace R) ⟨a, ⟨haS, rfl⟩⟩
le_sInf := fun _ _ h => le_sInf (α := TopologicalSpace R) <| forall_mem_image.2 h
