Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: characterize "eventually" in a subtype #7568

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: characterize "eventually" in a subtype #7568

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f00a71b
lemma
hrmacbeth Oct 8, 2023
40cc0b6
Update Mathlib/Topology/ContinuousOn.lean
ADedecker Jan 29, 2024
9e736fe
Merge remote-tracking branch 'origin/master' into HM-eventually_nhds_…
ADedecker Jan 29, 2024
8b26b5f
golf and frequently
ADedecker Jan 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions Mathlib/Topology/ContinuousOn.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,6 +505,14 @@ theorem preimage_coe_mem_nhds_subtype {s t : Set α} {a : s} : (↑) ⁻¹' t
rw [← map_nhds_subtype_val, mem_map]
#align preimage_coe_mem_nhds_subtype preimage_coe_mem_nhds_subtype

theorem eventually_nhds_subtype_if (s : Set α) (a : s) (P : α → Prop) :
(∀ᶠ x : s in 𝓝 a, P x) ↔ ∀ᶠ x in 𝓝[s] a, P x :=
preimage_coe_mem_nhds_subtype

theorem frequently_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) :
(∃ᶠ x : s in 𝓝 a, P x) ↔ ∃ᶠ x in 𝓝[s] a, P x :=
eventually_nhds_subtype_if s a (¬ P ·) |>.not

theorem tendsto_nhdsWithin_iff_subtype {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) :
Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := by
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]; rfl
Expand Down
Loading