Theorem: RegularOpens.cl_le_iff (LeanCourse/Lectures/Lecture11.lean)

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V U : RegularOpens X
C : Closeds X
⊢ cl U ≤ C ↔ U ≤ Closeds.int C
Tactic:
sorry
State after:
no goals