case tfae_1_iff_2
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ NoetherianSpace α ↔ WellFounded fun s t => s < t

α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
tfae_have 1 ↔ 2
case tfae_1_iff_4
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
tfae_have 1 ↔ 4
case tfae_1_to_3
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ NoetherianSpace α → ∀ (s : Set α), IsCompact s

α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
tfae_have 1 → 3
case tfae_3_to_4
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s

α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
tfae_3_to_4 : (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
tfae_have 3 → 4
no goals
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
tfae_3_to_4 : (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
tfae_finish
case tfae_1_iff_2
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ {a b : Opens α}, a > b ↔ Opens.compl a < Opens.compl b
case tfae_1_iff_2
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ NoetherianSpace α ↔ WellFounded fun s t => s < t
refine' (noetherianSpace_iff α).trans (Surjective.wellFounded_iff Opens.compl_bijective.2 _)
no goals
case tfae_1_iff_2
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ {a b : Opens α}, a > b ↔ Opens.compl a < Opens.compl b
exact (@OrderIso.compl (Set α)).lt_iff_lt.symm
no goals
case tfae_1_iff_4
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
exact noetherianSpace_iff_opens α
no goals
case tfae_1_to_3
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ NoetherianSpace α → ∀ (s : Set α), IsCompact s
exact @NoetherianSpace.isCompact α _
no goals
case tfae_3_to_4
α : Type u_1
β : Type ?u.1862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
exact fun h s => h s