[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
[PROOFSTEP]
let ⟨t, htx, htf⟩ := hf x
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
[PROOFSTEP]
refine ⟨t, htx, htf.preimage <| ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ InjOn (fun i => g i) ((fun i => g i) ⁻¹' {i | Set.Nonempty (f i ∩ t)})
[PROOFSTEP]
exact hg.mono fun i (hi : Set.Nonempty _) => hi.left
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
rcases hf a with ⟨U, haU, hfin⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
calc
  𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
  _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by simp only [mem_setOf_eq, iUnion_nonempty_self]
  _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := (nhdsWithin_biUnion hfin _ _)
  _ ≤ ⨆ i, 𝓝[f i ∩ U] a := (iSup₂_le_iSup _ _)
  _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ <| inter_subset_left _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
[PROOFSTEP]
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι) (_ : i ∈ {j | Set.Nonempty (f j ∩ U)}), f i ∩ U] a
[PROOFSTEP]
simp only [mem_setOf_eq, iUnion_nonempty_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ (i : ι), f i)
[PROOFSTEP]
rintro x -
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x
[PROOFSTEP]
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
by_cases hx : x ∈ closure (f i)
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
exact hc i _ hx
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx 
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
rw [hx]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))
[PROOFSTEP]
exact tendsto_bot
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i => closure (f i)
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
[PROOFSTEP]
rcases hf x with ⟨s, hsx, hsf⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
[PROOFSTEP]
refine' ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => _⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
i : ι
hi : i ∈ {i | Set.Nonempty ((fun i => closure (f i)) i ∩ interior s)}
⊢ i ∈ {i | Set.Nonempty (f i ∩ s)}
[PROOFSTEP]
exact (hi.mono isOpen_interior.closure_inter).of_closure.mono (inter_subset_inter_right _ interior_subset)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ (i : ι), f i) ↔ x ∈ ⋃ (i : ι), closure (f i)
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
⊢ IsClosed (⋃ (i : ι), f i)
[PROOFSTEP]
simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ ⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ ∈ 𝓝 x
[PROOFSTEP]
refine' IsOpen.mem_nhds _ (mem_iInter₂.2 fun i => id)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ)
[PROOFSTEP]
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
this : IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ)
[PROOFSTEP]
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
[PROOFSTEP]
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
choose U hUx hU using hf
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
choose N hN using fun x => (hU x).bddAbove
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X), N x ∈ upperBounds {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
[GOAL]
case hN
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X), N x ∈ upperBounds {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
exact fun x n hn y hy => by_contra fun hne => hn.lt.not_le <| hN x ⟨y, hne, hy⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
[GOAL]
case hN
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
exact fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
⊢ ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = (fun x => f (N x + 1) x) p.snd
[PROOFSTEP]
filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
⊢ ∀ (a : ℕ × X), a ∈ {x_1 | N x < x_1} ×ˢ U x → f a.fst a.snd = f (N a.snd + 1) a.snd
[PROOFSTEP]
rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩
[GOAL]
case h.mk.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (n, y).fst (n, y).snd = f (N (n, y).snd + 1) (n, y).snd
[PROOFSTEP]
calc
  f n y = f (N x + 1) y := hN _ _ hn _ hy
  _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
  _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ↑e)
⊢ LocallyFinite f
[PROOFSTEP]
simpa only [(· ∘ ·), e.apply_symm_apply] using h.comp_injective e.symm.injective
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : ι ⊕ ι' → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)
[PROOFSTEP]
simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr, preimage_setOf_eq, (· ∘ ·),
  eventually_and]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)
[PROOFSTEP]
rw [← (Equiv.optionEquivSumPUnit.{_, 0} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)
[PROOFSTEP]
simp only [locallyFinite_of_finite, and_true]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
[PROOFSTEP]
rfl
