feat: add CompleteAtomicBooleanAlgebra is order isomorphic to set of its atoms (#31724)

`CompleteAtomicBooleanAlgebra` is order isomorphic to the set of its atoms. This PR add a `OrderIso` definition that prove this fact.

Author: Jun2M

Mathlib/Order/Atoms.lean

@@ -703,6 +703,44 @@ instance {α} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α :=
 instance {α} [CompleteAtomicBooleanAlgebra α] : IsCoatomistic α :=
   isAtomistic_dual_iff_isCoatomistic.1 inferInstance
 
+theorem exists_mem_le_of_le_sSup_of_isAtom {α} [CompleteAtomicBooleanAlgebra α] {a}
+    (ha : IsAtom a) {s : Set α} (hs : a ≤ sSup s) : ∃ b ∈ s, a ≤ b := by
+  by_contra! hnle
+  have : ⨆ s₀ ∈ s, a ⊓ s₀ = ⊥ := by
+    simp only [iSup_eq_bot]
+    intro s₀ hs₀
+    simpa [hnle s₀ hs₀] using ha.le_iff.mp (inf_le_left (b := s₀))
+  obtain rfl := (inf_eq_left.mpr hs).symm.trans <| inf_sSup_eq.trans this
+  exact ha.1 rfl
+
+lemma eq_setOf_le_sSup_and_isAtom {α} [CompleteAtomicBooleanAlgebra α] {S : Set α}
+    (hS : ∀ a ∈ S, IsAtom a) : S = {a | a ≤ sSup S ∧ IsAtom a} := by
+  ext a
+  refine ⟨fun h => ⟨CompleteLattice.le_sSup S a h, hS a h⟩, fun ⟨hale, hatom⟩ => ?_⟩
+  obtain ⟨b, hbS, hba⟩ := exists_mem_le_of_le_sSup_of_isAtom hatom hale
+  obtain rfl | rfl := (hS b hbS).le_iff.mp hba
+  · simpa using hatom.1
+  assumption
+
+/--
+Representation theorem for complete atomic boolean algebras:
+For a complete atomic Boolean algebra `α`, `toSetOfIsAtom` is an order isomorphism
+between `α` and the set of subsets of its atoms.
+-/
+def toSetOfIsAtom {α} [CompleteAtomicBooleanAlgebra α] : α ≃o (Set {a : α // IsAtom a}) where
+  toFun A := {a | a ≤ A}
+  invFun S := sSup (Subtype.val '' S)
+  left_inv A := by simp [Subtype.coe_image]
+  right_inv S := by
+    have h : ∀ a ∈ Subtype.val '' S, IsAtom a := by
+      rintro a ⟨a', ha', rfl⟩
+      exact a'.prop
+    rw [← Subtype.val_injective.image_injective.eq_iff, eq_setOf_le_sSup_and_isAtom h]
+    ext a
+    simp
+  map_rel_iff' {a b} := by
+    simpa using le_iff_atom_le_imp.symm
+
 end CompleteAtomicBooleanAlgebra
 
 end Atomistic