case intro
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), ↑γ t ∈ F
⊢ x ∈ F ∧ y ∈ F
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F
rcases h with ⟨γ, γ_in⟩
case intro
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), ↑γ t ∈ F
this : ↑γ 0 ∈ F ∧ ↑γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F
case intro
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), ↑γ t ∈ F
⊢ x ∈ F ∧ y ∈ F
have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
no goals
case intro
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), ↑γ t ∈ F
this : ↑γ 0 ∈ F ∧ ↑γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F
simpa using this
no goals
X : Type u_1
Y : Type ?u.547721
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.547736
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), ↑γ t ∈ F
⊢ ↑γ 0 ∈ F ∧ ↑γ 1 ∈ F
constructor <;> apply γ_in