LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.RegularOpen

Auxiliary declarations for the Borel determinacy formalization.

theorem TopologicalSpace.Opens.le_def {X : Type u_1} [tX : TopologicalSpace X] {U V : Opens X} : U ≤ V ↔ ↑U ⊆ ↑V

@[simp]

theorem TopologicalSpace.Opens.coe_himp' {X : Type u_1} [tX : TopologicalSpace X] {U V : Opens X} : ↑(U ⇨ V) = interior (↑V ∪ (↑U)ᶜ)

@[simp]

theorem TopologicalSpace.Opens.coe_compl' {X : Type u_1} [tX : TopologicalSpace X] {U : Opens X} : ↑Uᶜ = interior (↑U)ᶜ

theorem TopologicalSpace.Opens.coe_compl_compl {X : Type u_1} [tX : TopologicalSpace X] {U : Opens X} : ↑Uᶜᶜ = interior (closure ↑U)

theorem TopologicalSpace.Opens.isRegular_iff {X : Type u_1} [tX : TopologicalSpace X] {U : Opens X} : Heyting.IsRegular U ↔ interior (closure ↑U) = ↑U

theorem interior_closure_interior_closure_eq_interior_closure {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : interior (closure (interior (closure A))) = interior (closure A)

theorem IsClosed.interior_isRegular {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} (hA : IsClosed A) : Heyting.IsRegular (TopologicalSpace.Opens.interior A)