α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)
rw [induced_generateFrom_eq]
case h
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ ∀ (s : Set α), s ∈ preimage f '' b → IsOpen s
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)
apply le_generateFrom
case h
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
case h
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ ∀ (s : Set α), s ∈ preimage f '' b → IsOpen s
simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
no goals
case h
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
⊢ ∀ (a : Set β), a ∈ b → IsOpen (f ⁻¹' a)
exact h