case path_connected_basis
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
⊢ ∀ (x : X), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
⊢ LocPathConnectedSpace X
constructor
case path_connected_basis
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
case path_connected_basis
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
⊢ ∀ (x : X), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
intro x
case path_connected_basis.h
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ ∀ (i : ι), p i → ∃ i', (i' ∈ 𝓝 x ∧ IsPathConnected i') ∧ id i' ⊆ s x i

case path_connected_basis.h'
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ ∀ (i' : Set X), i' ∈ 𝓝 x ∧ IsPathConnected i' → ∃ i, p i ∧ s x i ⊆ id i'
case path_connected_basis
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
apply (h x).to_hasBasis
case path_connected_basis.h
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
i : ι
pi : p i
⊢ ∃ i', (i' ∈ 𝓝 x ∧ IsPathConnected i') ∧ id i' ⊆ s x i
case path_connected_basis.h
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ ∀ (i : ι), p i → ∃ i', (i' ∈ 𝓝 x ∧ IsPathConnected i') ∧ id i' ⊆ s x i
intro i pi
no goals
case path_connected_basis.h
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
i : ι
pi : p i
⊢ ∃ i', (i' ∈ 𝓝 x ∧ IsPathConnected i') ∧ id i' ⊆ s x i
exact ⟨s x i, ⟨(h x).mem_of_mem pi, h' x i pi⟩, by rfl⟩
no goals
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
i : ι
pi : p i
⊢ id (s x i) ⊆ s x i
rfl
case path_connected_basis.h'.intro
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
U : Set X
U_in : U ∈ 𝓝 x
_hU : IsPathConnected U
⊢ ∃ i, p i ∧ s x i ⊆ id U
case path_connected_basis.h'
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
⊢ ∀ (i' : Set X), i' ∈ 𝓝 x ∧ IsPathConnected i' → ∃ i, p i ∧ s x i ⊆ id i'
rintro U ⟨U_in, _hU⟩
case path_connected_basis.h'.intro.intro.intro
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
U : Set X
U_in : U ∈ 𝓝 x
_hU : IsPathConnected U
i : ι
pi : p i
hi : s x i ⊆ U
⊢ ∃ i, p i ∧ s x i ⊆ id U
case path_connected_basis.h'.intro
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
U : Set X
U_in : U ∈ 𝓝 x
_hU : IsPathConnected U
⊢ ∃ i, p i ∧ s x i ⊆ id U
rcases(h x).mem_iff.mp U_in with ⟨i, pi, hi⟩
no goals
case path_connected_basis.h'.intro.intro.intro
X : Type u_1
Y : Type ?u.702092
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type u_2
F : Set X
p : ι → Prop
s : X → ι → Set X
h : ∀ (x : X), HasBasis (𝓝 x) p (s x)
h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)
x : X
U : Set X
U_in : U ∈ 𝓝 x
_hU : IsPathConnected U
i : ι
pi : p i
hi : s x i ⊆ U
⊢ ∃ i, p i ∧ s x i ⊆ id U
tauto