[GOAL]
α : Type u
g : Set (Set α)
a : α
⊢ 𝓝 a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
[PROOFSTEP]
letI := generateFrom g
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
[PROOFSTEP]
rw [nhds_def]
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
[PROOFSTEP]
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) ?_
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s
[PROOFSTEP]
refine le_iInf₂ fun s ⟨ha, hs⟩ => ?_
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
x✝ : s ∈ {s | a ∈ s ∧ IsOpen s}
ha : a ∈ s
hs : IsOpen s
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
[PROOFSTEP]
clear ‹s ∈ {s | a ∈ s ∧ IsOpen s}›
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
[PROOFSTEP]
induction hs with
| basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
| univ => exact le_top.trans_eq principal_univ.symm
| inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
| sUnion _ _ hS =>
  let ⟨t, htS, hat⟩ := ha
  exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
[GOAL]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
[PROOFSTEP]
induction hs with
| basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
| univ => exact le_top.trans_eq principal_univ.symm
| inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
| sUnion _ _ hS =>
  let ⟨t, htS, hat⟩ := ha
  exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
[GOAL]
case basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
hs : s✝ ∈ g
ha : a ∈ s✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s✝
[PROOFSTEP]

| basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
[GOAL]
case basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
hs : s✝ ∈ g
ha : a ∈ s✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s✝
[PROOFSTEP]
exact iInf₂_le _ ⟨ha, hs⟩
[GOAL]
case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 univ
[PROOFSTEP]

| univ => exact le_top.trans_eq principal_univ.symm
[GOAL]
case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 univ
[PROOFSTEP]
exact le_top.trans_eq principal_univ.symm
[GOAL]
case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
hs : a ∈ s✝ → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s✝
ht : a ∈ t✝ → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 (s✝ ∩ t✝)
[PROOFSTEP]

| inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
[GOAL]
case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
hs : a ∈ s✝ → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s✝
ht : a ∈ t✝ → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 (s✝ ∩ t✝)
[PROOFSTEP]
exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
[GOAL]
case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 (⋃₀ S✝)
[PROOFSTEP]

| sUnion _ _ hS =>
  let ⟨t, htS, hat⟩ := ha
  exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
[GOAL]
case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 (⋃₀ S✝)
[PROOFSTEP]
let ⟨t, htS, hat⟩ := ha
[GOAL]
case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s ≤ 𝓟 (⋃₀ S✝)
[PROOFSTEP]
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
[GOAL]
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
h : ∀ (s : Set β), s ∈ g → b ∈ s → m ⁻¹' s ∈ f
⊢ Tendsto m f (𝓝 b)
[PROOFSTEP]
rw [nhds_generateFrom]
[GOAL]
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
h : ∀ (s : Set β), s ∈ g → b ∈ s → m ⁻¹' s ∈ f
⊢ Tendsto m f (⨅ (s : Set β) (_ : s ∈ {s | b ∈ s ∧ s ∈ g}), 𝓟 s)
[PROOFSTEP]
exact tendsto_iInf.2 fun s => tendsto_iInf.2 fun ⟨hbs, hsg⟩ => tendsto_principal.2 <| h s hsg hbs
[GOAL]
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
⊢ 𝓝 a = n a
[PROOFSTEP]
letI := TopologicalSpace.mkOfNhds n
[GOAL]
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a = n a
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a ≤ n a
[PROOFSTEP]
intros s hs
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ n a ≤ 𝓝 a
[PROOFSTEP]
intros s hs
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
⊢ s ∈ 𝓝 a
[PROOFSTEP]
have h₀ : {b | s ∈ n b} ⊆ s := fun b hb => mem_pure.1 <| h₀ b hb
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀✝ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
h₀ : {b | s ∈ n b} ⊆ s
⊢ s ∈ 𝓝 a
[PROOFSTEP]
have h₁ : {b | s ∈ n b} ∈ 𝓝 a :=
  by
  refine' IsOpen.mem_nhds (fun b (hb : s ∈ n b) => _) hs
  rcases h₁ _ _ hb with ⟨t, ht, -, h⟩
  exact mem_of_superset ht h
[GOAL]
α : Type u
n : α → Filter α
a : α
h₀✝ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
h₀ : {b | s ∈ n b} ⊆ s
⊢ {b | s ∈ n b} ∈ 𝓝 a
[PROOFSTEP]
refine' IsOpen.mem_nhds (fun b (hb : s ∈ n b) => _) hs
[GOAL]
α : Type u
n : α → Filter α
a : α
h₀✝ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
h₀ : {b | s ∈ n b} ⊆ s
b : α
hb : s ∈ n b
⊢ {b | s ∈ n b} ∈ n b
[PROOFSTEP]
rcases h₁ _ _ hb with ⟨t, ht, -, h⟩
[GOAL]
case intro.intro.intro
α : Type u
n : α → Filter α
a : α
h₀✝ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
h₀ : {b | s ∈ n b} ⊆ s
b : α
hb : s ∈ n b
t : Set α
ht : t ∈ n b
h : ∀ (a' : α), a' ∈ t → s ∈ n a'
⊢ {b | s ∈ n b} ∈ n b
[PROOFSTEP]
exact mem_of_superset ht h
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀✝ : pure ≤ n
h₁✝ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ n a
h₀ : {b | s ∈ n b} ⊆ s
h₁ : {b | s ∈ n b} ∈ 𝓝 a
⊢ s ∈ 𝓝 a
[PROOFSTEP]
exact mem_of_superset h₁ h₀
[GOAL]
case a
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ 𝓝 a
⊢ s ∈ n a
[PROOFSTEP]
rcases mem_nhds_iff.1 hs with ⟨t, hts, ht, hat⟩
[GOAL]
case a.intro.intro.intro
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α) (s : Set α), s ∈ n a → ∃ t, t ∈ n a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ n a'
this : TopologicalSpace α := TopologicalSpace.mkOfNhds n
s : Set α
hs : s ∈ 𝓝 a
t : Set α
hts : t ⊆ s
ht : IsOpen t
hat : a ∈ t
⊢ s ∈ n a
[PROOFSTEP]
exact (n a).sets_of_superset (ht _ hat) hts
[GOAL]
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update pure a₀ l b
[PROOFSTEP]
refine' nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => _
[GOAL]
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
[PROOFSTEP]
rcases eq_or_ne a a₀ with (rfl | ha)
[GOAL]
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∃ t, t ∈ update pure a l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a l a'
[PROOFSTEP]
refine' ⟨s, hs, Subset.rfl, fun b hb => _⟩
[GOAL]
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b
[PROOFSTEP]
rcases eq_or_ne b a with (rfl | hb)
[GOAL]
case inl.inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b
[PROOFSTEP]
exact hs
[GOAL]
case inl.inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b
[PROOFSTEP]
rwa [update_noteq hb]
[GOAL]
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
[PROOFSTEP]
have hs' := hs
[GOAL]
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
[PROOFSTEP]
rw [update_noteq ha] at hs ⊢
[GOAL]
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ pure a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ pure a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
[PROOFSTEP]
exact ⟨{ a }, rfl, singleton_subset_iff.mpr hs, forall_eq.2 hs'⟩
[GOAL]
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
⊢ 𝓝 a = FilterBasis.filter (B a)
[PROOFSTEP]
rw [TopologicalSpace.nhds_mkOfNhds]
[GOAL]
case h₀
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
⊢ pure ≤ fun x => FilterBasis.filter (B x)
[PROOFSTEP]
intro x n hn
[GOAL]
case h₁
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
⊢ ∀ (a : α) (s : Set α),
    s ∈ FilterBasis.filter (B a) →
      ∃ t, t ∈ FilterBasis.filter (B a) ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ FilterBasis.filter (B a')
[PROOFSTEP]
intro x n hn
[GOAL]
case h₀
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ (fun x => FilterBasis.filter (B x)) x
⊢ n ∈ pure x
[PROOFSTEP]
obtain ⟨m, hm₁, hm₂⟩ := (B x).mem_filter_iff.mp hn
[GOAL]
case h₁
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
[PROOFSTEP]
obtain ⟨m, hm₁, hm₂⟩ := (B x).mem_filter_iff.mp hn
[GOAL]
case h₀.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ (fun x => FilterBasis.filter (B x)) x
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ n ∈ pure x
[PROOFSTEP]
exact hm₂ (h₀ _ _ hm₁)
[GOAL]
case h₁.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
[PROOFSTEP]
obtain ⟨n₁, hn₁, hn₂, hn₃⟩ := h₁ x m hm₁
[GOAL]
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
[PROOFSTEP]
refine' ⟨n₁, (B x).mem_filter_of_mem hn₁, hn₂.trans hm₂, fun x' hx' => (B x').mem_filter_iff.mp _⟩
[GOAL]
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
⊢ n ∈ FilterBasis.filter (B x')
[PROOFSTEP]
obtain ⟨n₂, hn₄, hn₅⟩ := hn₃ x' hx'
[GOAL]
case h₁.intro.intro.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
n₂ : Set α
hn₄ : n₂ ∈ B x'
hn₅ : n₂ ⊆ m
⊢ n ∈ FilterBasis.filter (B x')
[PROOFSTEP]
exact ⟨n₂, hn₄, hn₅.trans hm₂⟩
[GOAL]
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
h : IsOpen U
⊢ U = ∅ ∨ U = univ
[PROOFSTEP]
induction h with
| basic _ h => exact False.elim h
| univ => exact .inr rfl
| inter _ _ _ _ h₁ h₂ => rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
| sUnion _ _ ih => exact sUnion_mem_empty_univ ih
[GOAL]
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
h : IsOpen U
⊢ U = ∅ ∨ U = univ
[PROOFSTEP]
induction h with
| basic _ h => exact False.elim h
| univ => exact .inr rfl
| inter _ _ _ _ h₁ h₂ => rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
| sUnion _ _ ih => exact sUnion_mem_empty_univ ih
[GOAL]
case basic
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ : Set α
h : s✝ ∈ ↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ
[PROOFSTEP]

| basic _ h => exact False.elim h
[GOAL]
case basic
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ : Set α
h : s✝ ∈ ↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ
[PROOFSTEP]
exact False.elim h
[GOAL]
case univ
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ
[PROOFSTEP]

| univ => exact .inr rfl
[GOAL]
case univ
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ
[PROOFSTEP]
exact .inr rfl
[GOAL]
case inter
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ
[PROOFSTEP]

| inter _ _ _ _ h₁ h₂ => rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
[GOAL]
case inter
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ
[PROOFSTEP]
rcases h₁ with (rfl | rfl)
[GOAL]
case inter.inl
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) ∅
⊢ ∅ ∩ t✝ = ∅ ∨ ∅ ∩ t✝ = univ
[PROOFSTEP]
rcases h₂ with (rfl | rfl)
[GOAL]
case inter.inr
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) univ
⊢ univ ∩ t✝ = ∅ ∨ univ ∩ t✝ = univ
[PROOFSTEP]
rcases h₂ with (rfl | rfl)
[GOAL]
case inter.inl.inl
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
a✝¹ a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) ∅
⊢ ∅ ∩ ∅ = ∅ ∨ ∅ ∩ ∅ = univ
[PROOFSTEP]
simp
[GOAL]
case inter.inl.inr
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) ∅
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) univ
⊢ ∅ ∩ univ = ∅ ∨ ∅ ∩ univ = univ
[PROOFSTEP]
simp
[GOAL]
case inter.inr.inl
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) univ
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) ∅
⊢ univ ∩ ∅ = ∅ ∨ univ ∩ ∅ = univ
[PROOFSTEP]
simp
[GOAL]
case inter.inr.inr
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
a✝¹ a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) univ
⊢ univ ∩ univ = ∅ ∨ univ ∩ univ = univ
[PROOFSTEP]
simp
[GOAL]
case sUnion
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
ih : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
[PROOFSTEP]

| sUnion _ _ ih => exact sUnion_mem_empty_univ ih
[GOAL]
case sUnion
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
ih : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
[PROOFSTEP]
exact sUnion_mem_empty_univ ih
[GOAL]
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ U = ∅ ∨ U = univ → IsOpen U
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α✝ : Type ?u.10996
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
⊢ IsOpen ∅
case inr α✝ : Type ?u.10996 t t₁ t₂ : TopologicalSpace α✝ s : Set α✝ α : Type u_1 ⊢ IsOpen univ
[PROOFSTEP]
exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s✝ : Set α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
s : Set α
⊢ Dense s ↔ s = univ
[PROOFSTEP]
simp [dense_iff_closure_eq]
[GOAL]
α : Type u_2
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_1
f : ι → α
⊢ DenseRange f ↔ Surjective f
[PROOFSTEP]
rw [DenseRange, dense_discrete, range_iff_surjective]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s✝ : Set α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s
[PROOFSTEP]
rw [nhds_discrete, mem_pure]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s✝ : Set α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen s → IsOpen s
[PROOFSTEP]
rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds α t₂]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s✝ : Set α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ (∀ (a : α), a ∈ s → s ∈ 𝓝 a) → ∀ (a : α), a ∈ s → s ∈ 𝓝 a
[PROOFSTEP]
exact fun hs a ha => h _ (hs _ ha)
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x
[PROOFSTEP]
simp only [← singletons_open_iff_discrete, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x
[PROOFSTEP]
simp only [discreteTopology_iff_singleton_mem_nhds, ← nhds_neBot.le_pure_iff, le_pure_iff]
[GOAL]
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[{x}ᶜ] x = ⊥
[PROOFSTEP]
simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
⊢ ∀ (s t_1 : Set α),
    (fun s => ∃ s', IsOpen s' ∧ f ⁻¹' s' = s) s →
      (fun s => ∃ s', IsOpen s' ∧ f ⁻¹' s' = s) t_1 → (fun s => ∃ s', IsOpen s' ∧ f ⁻¹' s' = s) (s ∩ t_1)
[PROOFSTEP]
rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩
[GOAL]
case intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
s'₁ : Set β
hs₁ : IsOpen s'₁
s'₂ : Set β
hs₂ : IsOpen s'₂
⊢ ∃ s', IsOpen s' ∧ f ⁻¹' s' = f ⁻¹' s'₁ ∩ f ⁻¹' s'₂
[PROOFSTEP]
exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
S : Set (Set α)
h : ∀ (t_1 : Set α), t_1 ∈ S → (fun s => ∃ s', IsOpen s' ∧ f ⁻¹' s' = s) t_1
⊢ (fun s => ∃ s', IsOpen s' ∧ f ⁻¹' s' = s) (⋃₀ S)
[PROOFSTEP]
choose! g hgo hfg using h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
S : Set (Set α)
g : Set α → Set β
hgo : ∀ (t_1 : Set α), t_1 ∈ S → IsOpen (g t_1)
hfg : ∀ (t : Set α), t ∈ S → f ⁻¹' g t = t
⊢ ∃ s', IsOpen s' ∧ f ⁻¹' s' = ⋃₀ S
[PROOFSTEP]
refine ⟨⋃ s ∈ S, g s, isOpen_biUnion fun s hs => hgo s hs, ?_⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
S : Set (Set α)
g : Set α → Set β
hgo : ∀ (t_1 : Set α), t_1 ∈ S → IsOpen (g t_1)
hfg : ∀ (t : Set α), t ∈ S → f ⁻¹' g t = t
⊢ f ⁻¹' ⋃ (s : Set α) (_ : s ∈ S), g s = ⋃₀ S
[PROOFSTEP]
rw [preimage_iUnion₂, sUnion_eq_biUnion]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
S : Set (Set α)
g : Set α → Set β
hgo : ∀ (t_1 : Set α), t_1 ∈ S → IsOpen (g t_1)
hfg : ∀ (t : Set α), t ∈ S → f ⁻¹' g t = t
⊢ ⋃ (i : Set α) (_ : i ∈ S), f ⁻¹' g i = ⋃ (i : Set α) (_ : i ∈ S), i
[PROOFSTEP]
exact iUnion₂_congr hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
[PROOFSTEP]
letI := t.induced f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_induced_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s
[PROOFSTEP]
exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s
[PROOFSTEP]
simp only [preimage_compl, compl_inj_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
s : Set (Set β)
h : ∀ (t_1 : Set β), t_1 ∈ s → (fun s => IsOpen (f ⁻¹' s)) t_1
⊢ (fun s => IsOpen (f ⁻¹' s)) (⋃₀ s)
[PROOFSTEP]
simpa only [preimage_sUnion] using isOpen_biUnion h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a
[PROOFSTEP]
letI := TopologicalSpace.coinduced π ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a
[PROOFSTEP]
rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a
[PROOFSTEP]
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
t t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ TopologicalSpace.induced ↑e.symm = TopologicalSpace.coinduced ↑e
[PROOFSTEP]
ext t U
[GOAL]
case h.a.h.a
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen U ↔ IsOpen U
[PROOFSTEP]
rw [isOpen_induced_iff, isOpen_coinduced]
[GOAL]
case h.a.h.a
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ ↑e.symm ⁻¹' t_1 = U) ↔ IsOpen (↑e ⁻¹' U)
[PROOFSTEP]
simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, ← preimage_equiv_eq_image_symm]
[GOAL]
α✝ : 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)
[PROOFSTEP]
rw [induced_generateFrom_eq]
[GOAL]
α✝ : 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)
[PROOFSTEP]
apply le_generateFrom
[GOAL]
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
[PROOFSTEP]
simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
[GOAL]
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)
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t => 𝓝 a) t
[PROOFSTEP]
rw [le_nhds_iff]
[GOAL]
α : Type u
β : Type v
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
[PROOFSTEP]
exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
⊢ 𝓝 a = pure a ⊔ f
[PROOFSTEP]
letI := nhdsAdjoint a f
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f
[PROOFSTEP]
ext U
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ f
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ f
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ f
[PROOFSTEP]
rintro ⟨t, htU, ht, hat⟩
[GOAL]
case a.mp.intro.intro.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U t : Set α
htU : t ⊆ U
ht : IsOpen t
hat : a ∈ t
⊢ U ∈ pure a ⊔ f
[PROOFSTEP]
exact ⟨htU hat, mem_of_superset (ht hat) htU⟩
[GOAL]
case a.mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ pure a ⊔ f → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
rintro ⟨haU, hU⟩
[GOAL]
case a.mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
haU : U ∈ (pure a).sets
hU : U ∈ f.sets
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨U, Subset.rfl, fun _ => hU, haU⟩
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
⊢ 𝓝 b = pure b
[PROOFSTEP]
letI := nhdsAdjoint a f
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b ≤ pure b
[PROOFSTEP]
intro U hU
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ U ∈ 𝓝 b
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ b ∈ t
[PROOFSTEP]
use{ b }
[GOAL]
case h
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ {b} ⊆ U ∧ IsOpen {b} ∧ b ∈ {b}
[PROOFSTEP]
simp only [and_true_iff, singleton_subset_iff, mem_singleton]
[GOAL]
case h
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ b ∈ U ∧ IsOpen {b}
[PROOFSTEP]
refine' ⟨hU, fun ha => (h.symm ha).elim⟩
[GOAL]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ pure b ≤ 𝓝 b
[PROOFSTEP]
exact @pure_le_nhds α (nhdsAdjoint a f) b
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
⊢ IsOpen {b}
[PROOFSTEP]
letI := nhdsAdjoint a f
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ IsOpen {b}
[PROOFSTEP]
rw [isOpen_singleton_iff_nhds_eq_pure]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
[PROOFSTEP]
exact nhdsAdjoint_nhds_of_ne a f hb
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
[PROOFSTEP]
rw [le_iff_nhds]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) → 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
[PROOFSTEP]
constructor
[GOAL]
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f
[PROOFSTEP]
specialize h a
[GOAL]
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ 𝓝 a
⊢ 𝓝 a ≤ pure a ⊔ f
[PROOFSTEP]
rwa [nhdsAdjoint_nhds] at h
[GOAL]
case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ ∀ (b : α), b ≠ a → 𝓝 b = pure b
[PROOFSTEP]
intro b hb
[GOAL]
case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b = pure b
[PROOFSTEP]
apply le_antisymm _ (pure_le_nhds b)
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b ≤ pure b
[PROOFSTEP]
specialize h b
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
b : α
hb : b ≠ a
h : 𝓝 b ≤ 𝓝 b
⊢ 𝓝 b ≤ pure b
[PROOFSTEP]
rwa [nhdsAdjoint_nhds_of_ne a f hb] at h
[GOAL]
case mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b) → ∀ (x : α), 𝓝 x ≤ 𝓝 x
[PROOFSTEP]
rintro ⟨h, h'⟩ b
[GOAL]
case mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
⊢ 𝓝 b ≤ 𝓝 b
[PROOFSTEP]
by_cases hb : b = a
[GOAL]
case pos
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : b = a
⊢ 𝓝 b ≤ 𝓝 b
[PROOFSTEP]
rwa [hb, nhdsAdjoint_nhds]
[GOAL]
case neg
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : ¬b = a
⊢ 𝓝 b ≤ 𝓝 b
[PROOFSTEP]
simp [nhdsAdjoint_nhds_of_ne a f hb, h' b hb]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
[PROOFSTEP]
change _ ↔ _ ∧ ∀ b : α, b ≠ a → IsOpen { b }
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
[PROOFSTEP]
rw [le_nhdsAdjoint_iff', and_congr_right_iff]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ 𝓝 a ≤ pure a ⊔ f → ((∀ (b : α), b ≠ a → 𝓝 b = pure b) ↔ ∀ (b : α), b ≠ a → IsOpen {b})
[PROOFSTEP]
refine fun _ => forall_congr' fun b => ?_
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
x✝ : 𝓝 a ≤ pure a ⊔ f
b : α
⊢ b ≠ a → 𝓝 b = pure b ↔ b ≠ a → IsOpen {b}
[PROOFSTEP]
rw [@isOpen_singleton_iff_nhds_eq_pure α t b]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
g : γ → α
t₂ : TopologicalSpace β
t₁ : TopologicalSpace γ
⊢ Continuous g ↔ Continuous (f ∘ g)
[PROOFSTEP]
simp only [continuous_iff_le_induced, induced_compose]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous g ↔ Continuous (g ∘ f)
[PROOFSTEP]
simp only [continuous_iff_coinduced_le, coinduced_compose]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous f
⊢ Continuous f
[PROOFSTEP]
rw [continuous_iff_le_induced] at h₂ ⊢
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃
[PROOFSTEP]
exact le_trans h₁ h₂
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous f
⊢ Continuous f
[PROOFSTEP]
rw [continuous_iff_coinduced_le] at h₂ ⊢
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃
[PROOFSTEP]
exact le_trans h₂ h₁
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f
[PROOFSTEP]
simp only [continuous_iff_le_induced, sup_le_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
T : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ (t : TopologicalSpace α), t ∈ T → Continuous f
[PROOFSTEP]
simp only [continuous_iff_le_induced, sSup_le_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ (i : ι), Continuous f
[PROOFSTEP]
simp only [continuous_iff_le_induced, iSup_le_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f
[PROOFSTEP]
simp only [continuous_iff_coinduced_le, le_inf_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous f ↔ ∀ (t : TopologicalSpace β), t ∈ T → Continuous f
[PROOFSTEP]
simp only [continuous_iff_coinduced_le, le_sInf_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous f ↔ ∀ (i : ι), Continuous f
[PROOFSTEP]
simp only [continuous_iff_coinduced_le, le_iInf_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ ∃ u, u ∈ 𝓝 (f a) ∧ f ⁻¹' u ⊆ s
[PROOFSTEP]
letI := T.induced f
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ s ∈ 𝓝 a ↔ ∃ u, u ∈ 𝓝 (f a) ∧ f ⁻¹' u ⊆ s
[PROOFSTEP]
simp only [mem_nhds_iff, isOpen_induced_iff, exists_prop, Set.mem_setOf_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) → ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
[PROOFSTEP]
rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
v : Set α
openv : IsOpen v
usub : f ⁻¹' v ⊆ s
au : a ∈ f ⁻¹' v
⊢ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
[PROOFSTEP]
exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
[PROOFSTEP]
rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen v
amem : f a ∈ v
⊢ ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
[PROOFSTEP]
exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
[PROOFSTEP]
rw [mem_nhds_induced, mem_comap]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
h : ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))
x : β
⊢ 𝓝 x = 𝓝 x
[PROOFSTEP]
rw [h, nhds_induced]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : α → β
ι : Sort u_2
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)
[PROOFSTEP]
rw [nhds_induced, map_comap_of_surjective hf]
[GOAL]
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a
[PROOFSTEP]
rw [nhds_induced, Filter.map_comap, nhdsWithin]
[GOAL]
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)
[PROOFSTEP]
rw [nhds_induced, Filter.map_comap_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
[PROOFSTEP]
letI := t.induced f
[GOAL]
α : Type u_1
β : Type u_2
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
a : α
s : Set α
this : TopologicalSpace α := induced f t
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
[PROOFSTEP]
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
[PROOFSTEP]
letI := t.induced f
[GOAL]
α : Type u_1
β : Type u_2
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
s : Set α
this : TopologicalSpace α := induced f t
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
[PROOFSTEP]
simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ⨅ (s : Set Prop) (_ : s ∈ {s | False ∈ s ∧ s ∈ {{True}}}), 𝓟 s = ⊤
[PROOFSTEP]
simp [@and_comm (_ ∈ _)]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
l : Filter α
p : α → Prop
⊢ Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
l : Filter α
p : α → Prop
q : Prop
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
by_cases q
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
l : Filter α
p : α → Prop
q : Prop
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
by_cases q
[GOAL]
case pos
α : Type u_1
inst✝ : TopologicalSpace α
l : Filter α
p : α → Prop
q : Prop
h : q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : TopologicalSpace α
l : Filter α
p : α → Prop
q : Prop
h : ¬q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ Continuous p ↔ IsOpen {x | p x}
[PROOFSTEP]
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ (a : α), a ∈ {x | p x} → {x | p x} ∈ 𝓝 a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ s ∈ {s | IsOpen s} ↔ s ∈ {x | ∀ (i : ι), IsOpen x}
[PROOFSTEP]
simp [setOf_isOpen_iSup]
[GOAL]
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed s
[PROOFSTEP]
simp [← @isOpen_compl_iff _ (⨆ i, t i), ← @isOpen_compl_iff _ (t _), isOpen_iSup_iff]