α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
rw [continuousOn_iff']
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)) → ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
⊢ IsOpen (s ∩ f ⁻¹' t)
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
intro h t ht
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (s ∩ f ⁻¹' t)
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
⊢ IsOpen (s ∩ f ⁻¹' t)
rcases h t ht with ⟨u, u_open, hu⟩
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (u ∩ s)
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (s ∩ f ⁻¹' t)
rw [inter_comm, hu]
no goals
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (u ∩ s)
apply IsOpen.inter u_open hs
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)) → ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
intro h t ht
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
refine' ⟨s ∩ f ⁻¹' t, h t ht, _⟩
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.342559
δ : Type ?u.342562
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]