case mk
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ HasBasis (𝓝 { val := x, property := x_in }) (fun s => s ∈ 𝓝 { val := x, property := x_in } ∧ IsPathConnected s) id
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
⊢ ∀ (x : ↑U), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
rintro ⟨x, x_in⟩
case mk
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ HasBasis (comap Subtype.val (𝓝 x)) (fun s => s ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected s) id
case mk
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ HasBasis (𝓝 { val := x, property := x_in }) (fun s => s ∈ 𝓝 { val := x, property := x_in } ∧ IsPathConnected s) id
rw [nhds_subtype_eq_comap]
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ ∀ (t : Set ↑U), t ∈ comap Subtype.val (𝓝 x) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ t
case mk
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ HasBasis (comap Subtype.val (𝓝 x)) (fun s => s ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected s) id
constructor
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ V ∈ comap Subtype.val (𝓝 x) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
⊢ ∀ (t : Set ↑U), t ∈ comap Subtype.val (𝓝 x) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ t
intro V
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V) ↔
    ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ V ∈ comap Subtype.val (𝓝 x) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
rw [(HasBasis.comap ((↑) : U → X) (pathConnected_subset_basis h x_in)).mem_iff]
case mk.mem_iff'.mp
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V) →
    ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V

case mk.mem_iff'.mpr
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V) →
    ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V
case mk.mem_iff'
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V) ↔
    ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
constructor
case mk.mem_iff'.mp.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
W : Set X
hWV : Subtype.val ⁻¹' id W ⊆ V
W_in : W ∈ 𝓝 x
hW : IsPathConnected W
hWU : W ⊆ U
⊢ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
case mk.mem_iff'.mp
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V) →
    ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
rintro ⟨W, ⟨W_in, hW, hWU⟩, hWV⟩
no goals
case mk.mem_iff'.mp.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
W : Set X
hWV : Subtype.val ⁻¹' id W ⊆ V
W_in : W ∈ 𝓝 x
hW : IsPathConnected W
hWU : W ⊆ U
⊢ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
exact ⟨Subtype.val ⁻¹' W, ⟨⟨preimage_mem_comap W_in, hW.preimage_coe hWU⟩, hWV⟩⟩
case mk.mem_iff'.mpr.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x)
hW : IsPathConnected W
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V
case mk.mem_iff'.mpr
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V : Set ↑U
⊢ (∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V) →
    ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V
rintro ⟨W, ⟨W_in, hW⟩, hWV⟩
case mk.mem_iff'.mpr.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x)
hW : IsPathConnected W
⊢ Subtype.val ⁻¹' id (Subtype.val '' W) ⊆ V
case mk.mem_iff'.mpr.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x)
hW : IsPathConnected W
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V
refine'
  ⟨(↑) '' W,
    ⟨Filter.image_coe_mem_of_mem_comap (IsOpen.mem_nhds h x_in) W_in,
      hW.image continuous_subtype_val, Subtype.coe_image_subset U W⟩,
    _⟩
case mk.mem_iff'.mpr.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y✝ z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x✝ : X
x_in : x✝ ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x✝)
hW : IsPathConnected W
x : { x // x ∈ U }
y : ↑U
y_in : y ∈ W
hy : ↑y = ↑x
⊢ x ∈ V
case mk.mem_iff'.mpr.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x : X
x_in : x ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x)
hW : IsPathConnected W
⊢ Subtype.val ⁻¹' id (Subtype.val '' W) ⊆ V
rintro x ⟨y, ⟨y_in, hy⟩⟩
case mk.mem_iff'.mpr.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y✝ z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x✝ : X
x_in : x✝ ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x✝)
hW : IsPathConnected W
x : { x // x ∈ U }
y : ↑U
y_in : y ∈ W
hy : ↑y = ↑x
⊢ y ∈ V
case mk.mem_iff'.mpr.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y✝ z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x✝ : X
x_in : x✝ ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x✝)
hW : IsPathConnected W
x : { x // x ∈ U }
y : ↑U
y_in : y ∈ W
hy : ↑y = ↑x
⊢ x ∈ V
rw [← Subtype.coe_injective hy]
no goals
case mk.mem_iff'.mpr.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.705929
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y✝ z : X
ι : Type ?u.705944
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
h : IsOpen U
x✝ : X
x_in : x✝ ∈ U
V W : Set ↑U
hWV : id W ⊆ V
W_in : W ∈ comap Subtype.val (𝓝 x✝)
hW : IsPathConnected W
x : { x // x ∈ U }
y : ↑U
y_in : y ∈ W
hy : ↑y = ↑x
⊢ y ∈ V
tauto