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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ U ≤ V ↔ ↑U ⊆ ↑V
Tactic:
simp
State after:
no goals