case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us

case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us) → IsBasis B
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
constructor
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us, Us ⊆ B ∧ U = sSup Us
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
intro hB U
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us, Us ⊆ B ∧ U = sSup Us
refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
no goals
case mp
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
rfl
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ IsBasis B
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us) → IsBasis B
intro h
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ IsBasis B
rw [isBasis_iff_nbhd]
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
intro U x hx
case mpr.intro.intro
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
case mpr
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
rcases h U with ⟨Us, hUs, rfl⟩
case mpr.intro.intro.intro.intro
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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✝
case mpr.intro.intro
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
no goals
case mpr.intro.intro.intro.intro
ι : Type ?u.31277
α : Type u_1
β : Type ?u.31283
γ : Type ?u.31286
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✝
exact ⟨U, hUs Us, xU, le_sSup Us⟩