α : Type u_1
β : Type ?u.411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ (∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
α : Type u_1
β : Type ?u.411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
rw [noetherianSpace_iff, CompleteLattice.wellFounded_iff_isSupFiniteCompact,
  CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
no goals
α : Type u_1
β : Type ?u.411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ (∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
exact forall_congr' Opens.isCompactElement_iff