mathlib3 documentation

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.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
@[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.has_le.le.is_total {α : Type u} {β : Type v} {φ : ultrafilter α} [has_le β] [is_total β has_le.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]
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_ring β] :
Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_field {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_field β] :
Equations
@[protected, instance]
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 β) :
@[simp]
theorem filter.germ.const_max {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
@[simp]
theorem filter.germ.const_min {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
@[simp]
theorem filter.germ.const_abs {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] (x : β) :