Theorems · Theorem · general topology
Filter.Tendsto.congr_germ
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f g : β → γ} {l : Filter α} {l' : Filter β},
f =ᶠ[l'] g → ∀ {φ : α → β}, Filter.Tendsto φ l l' → ↑(f ∘ φ) = ↑(g ∘ φ)- Defined in
- Mathlib.Order.Filter.Germ.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.EventuallyEqstatement and proof · cited by 1,912
- Filter.Germstatement · cited by 102
- Filter.Germ.ofFunstatement · cited by 73
- Filter.EventuallyEq.comp_tendstoproof · cited by 5
- Filter.EventuallyEq.germ_eqproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Filter.Germ.Filter.Tendsto.congr_germproof · cited by 0