# mathlib3documentation

order.filter.filter_product

# Ultraproducts #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If φ is an ultrafilter, then the space of germs of functions f : α → β at φ is called the ultraproduct. In this file we prove properties of ultraproducts that rely on φ being an ultrafilter. Definitions and properties that work for any filter should go to order.filter.germ.

## Tags #

ultrafilter, ultraproduct

@[protected, instance]
def filter.germ.division_semiring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.division_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.semifield {α : Type u} {β : Type v} {φ : ultrafilter α} [semifield β] :
Equations
@[protected, instance]
def filter.germ.field {α : Type u} {β : Type v} {φ : ultrafilter α} [field β] :
field (φ.germ β)
Equations
theorem filter.germ.coe_lt {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {f g : α β} :
f < g ∀ᶠ (x : α) in φ, f x < g x
theorem filter.germ.coe_pos {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] [has_zero β] {f : α β} :
0 < f ∀ᶠ (x : α) in φ, 0 < f x
theorem filter.germ.const_lt {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {x y : β} :
x < y x < y
@[simp, norm_cast]
theorem filter.germ.const_lt_iff {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {x y : β} :
x < y x < y
theorem filter.germ.lt_def {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] :
@[protected, instance]
def filter.germ.has_sup {α : Type u} {β : Type v} {φ : ultrafilter α} [has_sup β] :
Equations
@[protected, instance]
def filter.germ.has_inf {α : Type u} {β : Type v} {φ : ultrafilter α} [has_inf β] :
Equations
@[simp, norm_cast]
theorem filter.germ.const_sup {α : Type u} {β : Type v} {φ : ultrafilter α} [has_sup β] (a b : β) :
(a b) = a b
@[simp, norm_cast]
theorem filter.germ.const_inf {α : Type u} {β : Type v} {φ : ultrafilter α} [has_inf β] (a b : β) :
(a b) = a b
@[protected, instance]
def filter.germ.semilattice_sup {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.semilattice_inf {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.lattice {α : Type u} {β : Type v} {φ : ultrafilter α} [lattice β] :
Equations
@[protected, instance]
def filter.germ.distrib_lattice {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.has_le.le.is_total {α : Type u} {β : Type v} {φ : ultrafilter α} [has_le β]  :
@[protected, instance]
noncomputable def filter.germ.linear_order {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] :

If φ is an ultrafilter then the ultraproduct is a linear order.

Equations
@[protected, instance]
def filter.germ.ordered_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_add_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_cancel_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_cancel_add_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_add_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_add_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_semiring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_comm_semiring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_ring β] :
Equations
@[protected, instance]
def filter.germ.ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.strict_ordered_semiring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.strict_ordered_comm_semiring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.strict_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
def filter.germ.strict_ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_field {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α}  :
Equations
theorem filter.germ.max_def {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : φ.germ β) :
theorem filter.germ.min_def {α : Type u} {β : Type v} {φ : ultrafilter α} [K : linear_order β] (x y : φ.germ β) :
theorem filter.germ.abs_def {α : Type u} {β : Type v} {φ : ultrafilter α} (x : φ.germ β) :
@[simp]
theorem filter.germ.const_max {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
y) =
@[simp]
theorem filter.germ.const_min {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
y) =
@[simp]
theorem filter.germ.const_abs {α : Type u} {β : Type v} {φ : ultrafilter α} (x : β) :