Filter.EventuallyEq.germ_eq
theorem Filter.EventuallyEq.germ_eq :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, l.EventuallyEq f g → ↑f = ↑g
This theorem, named `Filter.EventuallyEq.germ_eq`, is essentially an alias for the reverse direction of the theorem `Filter.Germ.coe_eq`. Given two functions `f` and `g` from a type `α` to a type `β`, and a filter `l` on `α`, it states that if `f` and `g` are eventually equal (i.e., they are equal almost everywhere with respect to the filter `l`), then the germ of `f` is equal to the germ of `g`. Here, "germ" refers to a class of functions that are equal almost everywhere with respect to a given filter. In other words, two functions are considered the same if they agree on the output for most elements of the input set, as defined by the filter.
More concisely: If functions `f` and `g` from type `α` to type `β` are eventually equal with respect to filter `l`, then their germs with respect to `l` are equal.
|
Filter.Germ.inductionOn₃
theorem Filter.Germ.inductionOn₃ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (f : l.Germ β) (g : l.Germ γ)
(h : l.Germ δ) {p : l.Germ β → l.Germ γ → l.Germ δ → Prop},
(∀ (f : α → β) (g : α → γ) (h : α → δ), p ↑f ↑g ↑h) → p f g h
The theorem `Filter.Germ.inductionOn₃` states that for every filter `l` on a type `α`, and for `Filter.Germ`s `f`, `g`, and `h` of types `β`, `γ`, and `δ` respectively, if a property `p` holds for every triple of functions `(f : α → β)`, `(g : α → γ)`, `(h : α → δ)`, then the property `p` also holds for the corresponding `Filter.Germ`s `f`, `g`, and `h`. This theorem provides a method for proving certain properties about germ of functions at a filter by reducing the problem to proving the property for all functions.
More concisely: The theorem `Filter.Germ.inductionOn₃` asserts that if a property `p` holds for all triples of functions `f : α → β`, `g : α → γ`, `h : α → δ`, then it holds for their corresponding `Filter.Germ`s.
|
Filter.Tendsto.germ_tendsto
theorem Filter.Tendsto.germ_tendsto :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β},
Filter.Tendsto f l lb → (↑f).Tendsto lb
This theorem, known as an alias of the reverse direction of `Filter.Germ.coe_tendsto`, states that for any two types `α` and `β`, any filter `l` on type `α`, any function `f` from `α` to `β`, and any filter `lb` on type `β`, if `f` tends towards `lb` along `l`, then the germ (the equivalence class of `f` under the equivalence relation of being eventually equal at `l`) also tends towards `lb`. In other words, if for every neighborhood `a` of `lb`, the preimage of `a` under `f` is a neighborhood in `l`, then the same holds for the germ of `f`.
More concisely: If a function `f` from type `α` to `β` tends towards a filter `lb` on `β` along a filter `l` on `α`, then the germ of `f` tends towards `lb`.
|
Filter.Germ.coe_eq
theorem Filter.Germ.coe_eq :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, ↑f = ↑g ↔ l.EventuallyEq f g
This theorem states that for any two functions 'f' and 'g' from a type 'α' to a type 'β', and any filter 'l' on 'α', the germs (elements in the ultrapower) of 'f' and 'g' are equal if and only if 'f' and 'g' are eventually equal almost everywhere with respect to the filter 'l'. In the context of this theorem, 'eventually equal almost everywhere' means that 'f' and 'g' are equal for all elements in the set, except possibly on a subset that the filter 'l' does not care about.
More concisely: The theorem asserts that functions from type 'α' to type 'β' have equal germs in the ultrapower with respect to filter 'l' if and only if they are almost everywhere equal with respect to 'l'.
|
Filter.Germ.inductionOn
theorem Filter.Germ.inductionOn :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} (f : l.Germ β) {p : l.Germ β → Prop}, (∀ (f : α → β), p ↑f) → p f
This theorem is about the induction principle on the space of germs of functions from `α` to `β` at a filter `l`. It states that for all types `α` and `β`, for all filters `l` on `α`, and for any germ `f` of functions from `α` to `β` at filter `l`, if a proposition `p` holds for the equivalence class of every function from `α` to `β` (represented by `↑f`), then the proposition `p` also holds for the germ `f`.
More concisely: If a proposition holds for the equivalence classes of functions from `α` to `β` at filter `l`, then it holds for the germ of any function `f` from `α` to `β` at filter `l`.
|
Filter.Germ.const_le
theorem Filter.Germ.const_le :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : LE β] {x y : β}, x ≤ y → ↑x ≤ ↑y
This theorem, `Filter.Germ.const_le`, states that for any types `α` and `β`, any filter `l` on `α`, any less-than-or-equal relation on `β`, and any two elements `x` and `y` of `β`, if `x` is less than or equal to `y` then the germ (or equivalence class) of `x`, denoted as `↑x`, is less than or equal to the germ of `y`, denoted as `↑y`, under the filter `l`. In other words, this relation preserves the order of elements when they are lifted to their germs in the context of a specific filter.
More concisely: For any filter $l$ on type $\alpha$, relation $R$ on type $\beta$, and elements $x, y$ of $\beta$ with $x R y$, we have $↑\_xl ≤ ↑\_yl$ in the quotient structure of the filter $l$ on $\alpha$.
|
Mathlib.Order.Filter.Germ._auxLemma.2
theorem Mathlib.Order.Filter.Germ._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, (↑f = ↑g) = l.EventuallyEq f g
This theorem, from the Mathlib library in the Order.Filter.Germ module, states that for any types `α` and `β`, a filter `l` on `α`, and two functions `f` and `g` from `α` to `β`, the assertion that the germ of `f` equals the germ of `g` is equivalent to saying that `f` equals `g` almost everywhere with respect to the filter `l`. In other words, if two functions are equal almost everywhere on a certain filter, their germs are also equal.
More concisely: For any types `α` and `β`, filter `l` on `α`, and functions `f` and `g` from `α` to `β`, the germs of `f` and `g` are equal if and only if `f` and `g` are equal almost everywhere with respect to `l`.
|
Filter.Germ.inductionOn₂
theorem Filter.Germ.inductionOn₂ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : l.Germ β) (g : l.Germ γ)
{p : l.Germ β → l.Germ γ → Prop}, (∀ (f : α → β) (g : α → γ), p ↑f ↑g) → p f g
The theorem `Filter.Germ.inductionOn₂` states that for all types `α`, `β`, and `γ`, given a filter `l` on `α`, and two germs of functions `f` and `g` at the filter `l` with codomains `β` and `γ` respectively, for all properties `p` over pairs of germs from `β` and `γ`, if the property `p` holds for all pairs of function representatives of the germs, then the property `p` also holds for the germs `f` and `g`. This theorem essentially allows us to prove properties about germs by proving them for their representative functions.
More concisely: Given a filter `l` on type `α`, if a property `p` holds for all pairs of representative functions of germs `f:` `α` -> `β` and `g:` `α` -> `γ` in the filter `l`, then property `p` holds for the germs `f` and `g` at the filter `l`.
|
Mathlib.Order.Filter.Germ._auxAddLemma.2
theorem Mathlib.Order.Filter.Germ._auxAddLemma.2 :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, (↑f = ↑g) = l.EventuallyEq f g
This theorem, named `Mathlib.Order.Filter.Germ._auxAddLemma.2`, is from the `Mathlib.Order.Filter.Germ` namespace of the Lean 4 Mathlib library. It states that for any two functions `f` and `g` from a type `α` to a type `β` and any filter `l` on `α`, the functions `f` and `g` being equal as germs (indicated by `↑f = ↑g`) is equivalent to the statement that `f` and `g` are eventually equal (`f =ᶠ[l] g`) with respect to the filter `l`. In other words, `f` and `g` being equal almost everywhere in terms of `l` is the same as them having the same germ at `l`.
More concisely: For any functions `f` and `g` from type `α` to type `β` and filter `l` on `α`, `↑f = ↑g` implies `f =ᶠ[l] g`. (Here, `↑f` denotes the germ of `f` at any point in `α`.)
|