α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
  intro t
  rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
  simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β), IsClosed s_1 → IsClosed (restrict s f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β), IsClosed s_1 → IsClosed (restrict s f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
simp only [this]
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
intro t
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsClosed t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' (f ⁻¹' t)) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.315580
δ : Type ?u.315583
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsClosed t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' (f ⁻¹' t)) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]