feat(topology/sets/order): Clopen upper sets (#12670)

Define `clopen_upper_set`, the type of clopen upper sets of an ordered topological space.

src/topology/sets/order.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import order.upper_lower
+import topology.sets.closeds
+
+/-!
+# Clopen upper sets
+
+In this file we define the type of clopen upper sets.
+-/
+
+open set topological_space
+
+variables {α β : Type*} [topological_space α] [has_le α] [topological_space β] [has_le β]
+
+/-! ### Compact open sets -/
+
+/-- The type of clopen upper sets of a topological space. -/
+structure clopen_upper_set (α : Type*) [topological_space α] [has_le α] extends clopens α :=
+(upper' : is_upper_set carrier)
+
+namespace clopen_upper_set
+
+instance : set_like (clopen_upper_set α) α :=
+{ coe := λ s, s.carrier,
+  coe_injective' := λ s t h, by { obtain ⟨⟨_, _⟩, _⟩ := s, obtain ⟨⟨_, _⟩, _⟩ := t, congr' } }
+
+lemma upper (s : clopen_upper_set α) : is_upper_set (s : set α) := s.upper'
+lemma clopen (s : clopen_upper_set α) : is_clopen (s : set α) := s.clopen'
+
+/-- Reinterpret a upper clopen as an upper set. -/
+@[simps] def to_upper_set (s : clopen_upper_set α) : upper_set α := ⟨s, s.upper⟩
+
+@[ext] protected lemma ext {s t : clopen_upper_set α} (h : (s : set α) = t) : s = t :=
+set_like.ext' h
+
+@[simp] lemma coe_mk (s : clopens α) (h) : (mk s h : set α) = s := rfl
+
+instance : has_sup (clopen_upper_set α) :=
+⟨λ s t, ⟨s.to_clopens ⊔ t.to_clopens, s.upper.union t.upper⟩⟩
+instance : has_inf (clopen_upper_set α) :=
+⟨λ s t, ⟨s.to_clopens ⊓ t.to_clopens, s.upper.inter t.upper⟩⟩
+instance : has_top (clopen_upper_set α) := ⟨⟨⊤, is_upper_set_univ⟩⟩
+instance : has_bot (clopen_upper_set α) := ⟨⟨⊥, is_upper_set_empty⟩⟩
+
+instance : lattice (clopen_upper_set α) :=
+set_like.coe_injective.lattice _ (λ _ _, rfl) (λ _ _, rfl)
+
+instance : bounded_order (clopen_upper_set α) :=
+bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl
+
+@[simp] lemma coe_sup (s t : clopen_upper_set α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
+@[simp] lemma coe_inf (s t : clopen_upper_set α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
+@[simp] lemma coe_top : (↑(⊤ : clopen_upper_set α) : set α) = univ := rfl
+@[simp] lemma coe_bot : (↑(⊥ : clopen_upper_set α) : set α) = ∅ := rfl
+
+instance : inhabited (clopen_upper_set α) := ⟨⊥⟩
+
+end clopen_upper_set