α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
⊢ IsQuasiSeparated (f '' s)
intro U V hU hU' hU'' hV hV' hV''
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)

case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s

case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
convert
  (H (f ⁻¹' U) (f ⁻¹' V)
    ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image h.continuous
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)
symm
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V ⊆ Set.range f
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
no goals
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V ⊆ Set.range f
exact (Set.inter_subset_left _ _).trans (hU.trans (Set.image_subset_range _ _))
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ x ∈ s
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s
intro x hx
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ x ∈ s
rw [← (h.inj.injOn _).mem_image_iff (Set.subset_univ _) trivial]
no goals
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s
exact hU hx
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' U))
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)
rw [h.isCompact_iff_isCompact_image]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U) = U
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' U))
convert hU''
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ⊆ Set.range f
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U) = U
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
no goals
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ⊆ Set.range f
exact hU.trans (Set.image_subset_range _ _)
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s
intro x hx
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s
rw [← (h.inj.injOn _).mem_image_iff (Set.subset_univ _) trivial]
no goals
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s
exact hV hx
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' V))
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)
rw [h.isCompact_iff_isCompact_image]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' V) = V
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' V))
convert hV''
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ V ⊆ Set.range f
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' V) = V
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
no goals
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : Embedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ V ⊆ Set.range f
exact hV.trans (Set.image_subset_range _ _)