[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝² x✝¹ : Opens α
carrier✝¹ : Set α
is_open'✝¹ : IsOpen carrier✝¹
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
x✝ : { carrier := carrier✝¹, is_open' := is_open'✝¹ }.carrier = { carrier := carrier✝, is_open' := is_open'✝ }.carrier
⊢ { carrier := carrier✝¹, is_open' := is_open'✝¹ } = { carrier := carrier✝, is_open' := is_open'✝ }
[PROOFSTEP]
congr
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
s : ι → Opens α
⊢ ↑(⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)
[PROOFSTEP]
simp [iSup]
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i
[PROOFSTEP]
rw [← SetLike.mem_coe]
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u, u ∈ Us ∧ x ∈ u
[PROOFSTEP]
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
src✝ : CompleteLattice (Opens α) := inferInstanceAs (CompleteLattice (Opens α))
a : Opens α
s : Set (Opens α)
⊢ ↑(a ⊓ sSup s) = ↑(⨆ (b : Opens α) (_ : b ∈ s), a ⊓ b)
[PROOFSTEP]
simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen (range (inclusion (_ : ↑U ⊆ ↑V)))
[PROOFSTEP]
rw [Set.range_inclusion i]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}
[PROOFSTEP]
exact U.isOpen.preimage continuous_subtype_val
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U : Opens α
⊢ ¬Set.Nonempty ↑U ↔ U = ⊥
[PROOFSTEP]
rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U : Opens α
⊢ U ≠ ⊥ ↔ Set.Nonempty ↑U
[PROOFSTEP]
rw [Ne.def, ← not_nonempty_iff_eq_bot, not_not]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
t : TopologicalSpace α
h : t = ⊤
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
letI : TopologicalSpace α := ⊤
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
rw [← coe_eq_empty, ← coe_eq_univ, ← isOpen_top_iff]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U
[PROOFSTEP]
exact U.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U) → IsBasis B
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
rintro ⟨sU, hU⟩ x hx
[GOAL]
case mp.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
refine' ⟨V, H₁, _⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
cases V
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : ↑{ carrier := carrier✝, is_open' := is_open'✝ } = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
dsimp at H₂ 
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
subst H₂
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
exact hsV
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds _ _
[GOAL]
case mpr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (u : Set α), u ∈ SetLike.coe '' B → IsOpen u
[PROOFSTEP]
rintro sU ⟨U, -, rfl⟩
[GOAL]
case mpr.refine'_1.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen ↑U
[PROOFSTEP]
exact U.2
[GOAL]
case mpr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ SetLike.coe '' B ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro x sU hx hsU
[GOAL]
case mpr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
[PROOFSTEP]
rcases@h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
[GOAL]
case mpr.refine'_2.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
[PROOFSTEP]
exact ⟨V, ⟨V, hV, rfl⟩, H⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
intro hB U
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
refine ⟨{V : Opens α | V ∈ B ∧ V ≤ U}, fun U hU => hU.left, ext ?_⟩
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})
[PROOFSTEP]
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃₀ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U} = ⋃ (i : Opens α) (_ : i ∈ {V | V ∈ B ∧ V ≤ U}), ↑i
[PROOFSTEP]
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⨆ (b : Opens α) (_ : b ∈ B) (_ : ↑b ⊆ ↑U), ↑b = ⨆ (i : Opens α) (_ : i ∈ B) (_ : i ≤ U), ↑i
[PROOFSTEP]
rfl
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us) → IsBasis B
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ IsBasis B
[PROOFSTEP]
rw [isBasis_iff_nbhd]
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
intro U x hx
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
rcases h U with ⟨Us, hUs, rfl⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ sSup Us
[PROOFSTEP]
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
[GOAL]
case mpr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
x : α
Us✝ : Set (Opens α)
hUs : Us✝ ⊆ B
hx : x ∈ sSup Us✝
U : Opens α
Us : U ∈ Us✝
xU : x ∈ U
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ sSup Us✝
[PROOFSTEP]
exact ⟨U, hUs Us, xU, le_sSup Us⟩
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), ↑(b i)
[PROOFSTEP]
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
[GOAL]
case hb
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)
[PROOFSTEP]
convert (config := { transparency := .default }) hb
[GOAL]
case h.e'_3
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b
[PROOFSTEP]
simp
[GOAL]
case hb'
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier
[PROOFSTEP]
exact hb'
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ CompleteLattice.IsCompactElement s ↔ IsCompact ↑s
[PROOFSTEP]
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
refine' ⟨_, fun H ι U hU => _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
introv H hU hU'
[GOAL]
case refine'_1
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ s ≤ ⨆ (i : ι), { carrier := U i, is_open' := (_ : IsOpen (U i)) }
[PROOFSTEP]
simpa
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
refine' ⟨t, Set.Subset.trans ht _⟩
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ↑(Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
rw [coe_finset_sup, Finset.sup_eq_iSup]
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ⨆ (a : ι) (_ : a ∈ t), (SetLike.coe ∘ fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) a ⊆
    ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ Finset.sup t U
[PROOFSTEP]
obtain ⟨t, ht⟩ := H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ (i : ι), (fun i => ↑(U i)) i
[PROOFSTEP]
simpa using show (s : Set α) ⊆ ↑(iSup U) from hU
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∃ t, s ≤ Finset.sup t U
[PROOFSTEP]
refine' ⟨t, Set.Subset.trans ht _⟩
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ⋃ (i : ι) (_ : i ∈ t), ↑(U i) ⊆ ↑(Finset.sup t U)
[PROOFSTEP]
simp only [Set.iUnion_subset_iff]
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → ↑(U i) ⊆ ↑(Finset.sup t U)
[PROOFSTEP]
show ∀ i ∈ t, U i ≤ t.sup U
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → U i ≤ Finset.sup t U
[PROOFSTEP]
exact fun i => Finset.le_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
s : Set (Opens β)
⊢ ↑(InfHom.toFun
        {
            toInfHom :=
              { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                map_inf' :=
                  (_ :
                    ∀ (a b : Opens β),
                      (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                        (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b)) },
            map_top' :=
              (_ :
                InfHom.toFun
                    { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                      map_inf' :=
                        (_ :
                          ∀ (a b : Opens β),
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                              (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                (a ⊓ b)) }
                    ⊤ =
                  InfHom.toFun
                    { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                      map_inf' :=
                        (_ :
                          ∀ (a b : Opens β),
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                              (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                (a ⊓ b)) }
                    ⊤) }.toInfHom
        (sSup s)) =
    ↑(sSup
        ({
                toInfHom :=
                  { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                    map_inf' :=
                      (_ :
                        ∀ (a b : Opens β),
                          (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b)) },
                map_top' :=
                  (_ :
                    InfHom.toFun
                        { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                          map_inf' :=
                            (_ :
                              ∀ (a b : Opens β),
                                (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b) =
                                  (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b)) }
                        ⊤ =
                      InfHom.toFun
                        { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                          map_inf' :=
                            (_ :
                              ∀ (a b : Opens β),
                                (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b) =
                                  (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b)) }
                        ⊤) }.toInfHom.toFun ''
          s))
[PROOFSTEP]
simp only [coe_sSup, preimage_iUnion, biUnion_image, coe_mk]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
              invFun := ↑(comap (Homeomorph.toContinuousMap f)),
              left_inv :=
                (_ :
                  ∀ (U : Opens α),
                    ↑(comap (Homeomorph.toContinuousMap f))
                        (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                      U),
              right_inv :=
                (_ :
                  ∀ (U : Opens β),
                    ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                        (↑(comap (Homeomorph.toContinuousMap f)) U) =
                      U) }
          a ≤
        ↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
              invFun := ↑(comap (Homeomorph.toContinuousMap f)),
              left_inv :=
                (_ :
                  ∀ (U : Opens α),
                    ↑(comap (Homeomorph.toContinuousMap f))
                        (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                      U),
              right_inv :=
                (_ :
                  ∀ (U : Opens β),
                    ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                        (↑(comap (Homeomorph.toContinuousMap f)) U) =
                      U) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp only [← SetLike.coe_subset_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑(↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
                invFun := ↑(comap (Homeomorph.toContinuousMap f)),
                left_inv :=
                  (_ :
                    ∀ (U : Opens α),
                      ↑(comap (Homeomorph.toContinuousMap f))
                          (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                        U),
                right_inv :=
                  (_ :
                    ∀ (U : Opens β),
                      ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                          (↑(comap (Homeomorph.toContinuousMap f)) U) =
                        U) }
            a) ⊆
        ↑(↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
                invFun := ↑(comap (Homeomorph.toContinuousMap f)),
                left_inv :=
                  (_ :
                    ∀ (U : Opens α),
                      ↑(comap (Homeomorph.toContinuousMap f))
                          (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                        U),
                right_inv :=
                  (_ :
                    ∀ (U : Opens β),
                      ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                          (↑(comap (Homeomorph.toContinuousMap f)) U) =
                        U) }
            b) ↔
      ↑a ⊆ ↑b
[PROOFSTEP]
exact f.symm.surjective.preimage_subset_preimage_iff
