order.filter.filter_product

source

@[protected, instance]

def filter.germ.division_semiring {α : Type u} {β : Type v} {φ : ultrafilter α} [division_semiring β] :

division_semiring (↑φ.germ β)

Equations

filter.germ.division_semiring = {add := semiring.add filter.germ.semiring, add_assoc := _, zero := semiring.zero filter.germ.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul filter.germ.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul filter.germ.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one filter.germ.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast filter.germ.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow filter.germ.semiring, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv filter.germ.div_inv_monoid, div := div_inv_monoid.div filter.germ.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow filter.germ.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

@[protected, instance]

def filter.germ.division_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [division_ring β] :

division_ring (↑φ.germ β)

Equations

filter.germ.division_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := division_semiring.inv filter.germ.division_semiring, div := division_semiring.div filter.germ.division_semiring, div_eq_mul_inv := _, zpow := division_semiring.zpow filter.germ.division_semiring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (↑φ.germ β)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (↑φ.germ β)), qsmul_eq_mul' := _}

source

@[protected, instance]

def filter.germ.semifield {α : Type u} {β : Type v} {φ : ultrafilter α} [semifield β] :

semifield (↑φ.germ β)

Equations

filter.germ.semifield = {add := comm_semiring.add filter.germ.comm_semiring, add_assoc := _, zero := comm_semiring.zero filter.germ.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul filter.germ.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul filter.germ.comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one filter.germ.comm_semiring, one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast filter.germ.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow filter.germ.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, inv := division_semiring.inv filter.germ.division_semiring, div := division_semiring.div filter.germ.division_semiring, div_eq_mul_inv := _, zpow := division_semiring.zpow filter.germ.division_semiring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

@[protected, instance]

def filter.germ.field {α : Type u} {β : Type v} {φ : ultrafilter α} [field β] :

field (↑φ.germ β)

Equations

filter.germ.field = {add := comm_ring.add filter.germ.comm_ring, add_assoc := _, zero := comm_ring.zero filter.germ.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul filter.germ.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg filter.germ.comm_ring, sub := comm_ring.sub filter.germ.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul filter.germ.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast filter.germ.comm_ring, nat_cast := comm_ring.nat_cast filter.germ.comm_ring, one := comm_ring.one filter.germ.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul filter.germ.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow filter.germ.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv filter.germ.division_ring, div := division_ring.div filter.germ.division_ring, div_eq_mul_inv := _, zpow := division_ring.zpow filter.germ.division_ring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast filter.germ.division_ring, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul filter.germ.division_ring, qsmul_eq_mul' := _}

source

theorem filter.germ.coe_lt {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {f g : α → β} :

↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x

source

theorem filter.germ.coe_pos {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] [has_zero β] {f : α → β} :

0 < ↑f ↔ ∀ᶠ (x : α) in ↑φ, 0 < f x

source

theorem filter.germ.const_lt {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {x y : β} :

x ≤ y → ↑x ≤ ↑y

source

theorem filter.germ.const_lt_iff {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] {x y : β} :

↑x < ↑y ↔ x < y

source

theorem filter.germ.lt_def {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] :

has_lt.lt = filter.germ.lift_rel has_lt.lt

source

@[protected, instance]

def filter.germ.has_sup {α : Type u} {β : Type v} {φ : ultrafilter α} [has_sup β] :

has_sup (↑φ.germ β)

Equations

filter.germ.has_sup = {sup := filter.germ.map₂ has_sup.sup}

source

@[protected, instance]

def filter.germ.has_inf {α : Type u} {β : Type v} {φ : ultrafilter α} [has_inf β] :

has_inf (↑φ.germ β)

Equations

filter.germ.has_inf = {inf := filter.germ.map₂ has_inf.inf}

source

@[simp, norm_cast]

theorem filter.germ.const_sup {α : Type u} {β : Type v} {φ : ultrafilter α} [has_sup β] (a b : β) :

↑(a ⊔ b) = ↑a ⊔ ↑b

source

@[simp, norm_cast]

theorem filter.germ.const_inf {α : Type u} {β : Type v} {φ : ultrafilter α} [has_inf β] (a b : β) :

↑(a ⊓ b) = ↑a ⊓ ↑b

source

@[protected, instance]

def filter.germ.semilattice_sup {α : Type u} {β : Type v} {φ : ultrafilter α} [semilattice_sup β] :

semilattice_sup (↑φ.germ β)

Equations

filter.germ.semilattice_sup = {sup := has_sup.sup filter.germ.has_sup, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

def filter.germ.semilattice_inf {α : Type u} {β : Type v} {φ : ultrafilter α} [semilattice_inf β] :

semilattice_inf (↑φ.germ β)

Equations

filter.germ.semilattice_inf = {inf := has_inf.inf filter.germ.has_inf, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def filter.germ.lattice {α : Type u} {β : Type v} {φ : ultrafilter α} [lattice β] :

lattice (↑φ.germ β)

Equations

filter.germ.lattice = {sup := semilattice_sup.sup filter.germ.semilattice_sup, le := semilattice_sup.le filter.germ.semilattice_sup, lt := semilattice_sup.lt filter.germ.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf filter.germ.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def filter.germ.distrib_lattice {α : Type u} {β : Type v} {φ : ultrafilter α} [distrib_lattice β] :

distrib_lattice (↑φ.germ β)

Equations

filter.germ.distrib_lattice = {sup := semilattice_sup.sup filter.germ.semilattice_sup, le := semilattice_sup.le filter.germ.semilattice_sup, lt := semilattice_sup.lt filter.germ.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf filter.germ.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected, instance]

def filter.germ.has_le.le.is_total {α : Type u} {β : Type v} {φ : ultrafilter α} [has_le β] [is_total β has_le.le] :

is_total (↑φ.germ β) has_le.le

source

@[protected, instance]

noncomputable def filter.germ.linear_order {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] :

linear_order (↑φ.germ β)

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

Equations

filter.germ.linear_order = lattice.to_linear_order (↑φ.germ β)

source

@[protected, instance]

def filter.germ.ordered_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_comm_monoid β] :

ordered_comm_monoid (↑φ.germ β)

Equations

filter.germ.ordered_comm_monoid = {mul := comm_monoid.mul filter.germ.comm_monoid, mul_assoc := _, one := comm_monoid.one filter.germ.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow filter.germ.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

@[protected, instance]

def filter.germ.ordered_add_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_add_comm_monoid β] :

ordered_add_comm_monoid (↑φ.germ β)

Equations

filter.germ.ordered_add_comm_monoid = {add := add_comm_monoid.add filter.germ.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero filter.germ.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul filter.germ.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

source

@[protected, instance]

def filter.germ.ordered_cancel_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_cancel_comm_monoid β] :

ordered_cancel_comm_monoid (↑φ.germ β)

Equations

filter.germ.ordered_cancel_comm_monoid = {mul := ordered_comm_monoid.mul filter.germ.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one filter.germ.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow filter.germ.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

@[protected, instance]

def filter.germ.ordered_cancel_add_comm_monoid {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_cancel_add_comm_monoid β] :

ordered_cancel_add_comm_monoid (↑φ.germ β)

Equations

filter.germ.ordered_cancel_add_comm_monoid = {add := ordered_add_comm_monoid.add filter.germ.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero filter.germ.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul filter.germ.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

@[protected, instance]

def filter.germ.ordered_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_comm_group β] :

ordered_comm_group (↑φ.germ β)

Equations

filter.germ.ordered_comm_group = {mul := ordered_cancel_comm_monoid.mul filter.germ.ordered_cancel_comm_monoid, mul_assoc := _, one := ordered_cancel_comm_monoid.one filter.germ.ordered_cancel_comm_monoid, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow filter.germ.ordered_cancel_comm_monoid, npow_zero' := _, npow_succ' := _, inv := comm_group.inv filter.germ.comm_group, div := comm_group.div filter.germ.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow filter.germ.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_cancel_comm_monoid.le filter.germ.ordered_cancel_comm_monoid, lt := ordered_cancel_comm_monoid.lt filter.germ.ordered_cancel_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

@[protected, instance]

def filter.germ.ordered_add_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_add_comm_group β] :

ordered_add_comm_group (↑φ.germ β)

Equations

filter.germ.ordered_add_comm_group = {add := ordered_cancel_add_comm_monoid.add filter.germ.ordered_cancel_add_comm_monoid, add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero filter.germ.ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul filter.germ.ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg filter.germ.add_comm_group, sub := add_comm_group.sub filter.germ.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul filter.germ.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le filter.germ.ordered_cancel_add_comm_monoid, lt := ordered_cancel_add_comm_monoid.lt filter.germ.ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

source

@[protected, instance]

noncomputable def filter.germ.linear_ordered_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_comm_group β] :

linear_ordered_comm_group (↑φ.germ β)

Equations

filter.germ.linear_ordered_comm_group = {mul := ordered_comm_group.mul filter.germ.ordered_comm_group, mul_assoc := _, one := ordered_comm_group.one filter.germ.ordered_comm_group, one_mul := _, mul_one := _, npow := ordered_comm_group.npow filter.germ.ordered_comm_group, npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv filter.germ.ordered_comm_group, div := ordered_comm_group.div filter.germ.ordered_comm_group, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow filter.germ.ordered_comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_group.le filter.germ.ordered_comm_group, lt := ordered_comm_group.lt filter.germ.ordered_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le filter.germ.linear_order, decidable_eq := linear_order.decidable_eq filter.germ.linear_order, decidable_lt := linear_order.decidable_lt filter.germ.linear_order, max := linear_order.max filter.germ.linear_order, max_def := _, min := linear_order.min filter.germ.linear_order, min_def := _}

source

@[protected, instance]

noncomputable def filter.germ.linear_ordered_add_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] :

linear_ordered_add_comm_group (↑φ.germ β)

Equations

filter.germ.linear_ordered_add_comm_group = {add := ordered_add_comm_group.add filter.germ.ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero filter.germ.ordered_add_comm_group, zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul filter.germ.ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg filter.germ.ordered_add_comm_group, sub := ordered_add_comm_group.sub filter.germ.ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul filter.germ.ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le filter.germ.ordered_add_comm_group, lt := ordered_add_comm_group.lt filter.germ.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le filter.germ.linear_order, decidable_eq := linear_order.decidable_eq filter.germ.linear_order, decidable_lt := linear_order.decidable_lt filter.germ.linear_order, max := linear_order.max filter.germ.linear_order, max_def := _, min := linear_order.min filter.germ.linear_order, min_def := _}

source

@[protected, instance]

def filter.germ.ordered_semiring {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_semiring β] :

ordered_semiring (↑φ.germ β)

Equations

filter.germ.ordered_semiring = {add := semiring.add filter.germ.semiring, add_assoc := _, zero := semiring.zero filter.germ.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul filter.germ.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul filter.germ.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one filter.germ.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast filter.germ.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow filter.germ.semiring, npow_zero' := _, npow_succ' := _, le := ordered_add_comm_monoid.le filter.germ.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt filter.germ.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}

source

@[protected, instance]

def filter.germ.ordered_comm_semiring {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_comm_semiring β] :

ordered_comm_semiring (↑φ.germ β)

Equations

filter.germ.ordered_comm_semiring = {add := ordered_semiring.add filter.germ.ordered_semiring, add_assoc := _, zero := ordered_semiring.zero filter.germ.ordered_semiring, zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul filter.germ.ordered_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_semiring.mul filter.germ.ordered_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ordered_semiring.one filter.germ.ordered_semiring, one_mul := _, mul_one := _, nat_cast := ordered_semiring.nat_cast filter.germ.ordered_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := ordered_semiring.npow filter.germ.ordered_semiring, npow_zero' := _, npow_succ' := _, le := ordered_semiring.le filter.germ.ordered_semiring, lt := ordered_semiring.lt filter.germ.ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}

source

@[protected, instance]

def filter.germ.ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_ring β] :

ordered_ring (↑φ.germ β)

Equations

filter.germ.ordered_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le filter.germ.ordered_add_comm_group, lt := ordered_add_comm_group.lt filter.germ.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _}

source

@[protected, instance]

def filter.germ.ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [ordered_comm_ring β] :

ordered_comm_ring (↑φ.germ β)

Equations

filter.germ.ordered_comm_ring = {add := ordered_ring.add filter.germ.ordered_ring, add_assoc := _, zero := ordered_ring.zero filter.germ.ordered_ring, zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul filter.germ.ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg filter.germ.ordered_ring, sub := ordered_ring.sub filter.germ.ordered_ring, sub_eq_add_neg := _, zsmul := ordered_ring.zsmul filter.germ.ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ordered_ring.int_cast filter.germ.ordered_ring, nat_cast := ordered_ring.nat_cast filter.germ.ordered_ring, one := ordered_ring.one filter.germ.ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ordered_ring.mul filter.germ.ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ordered_ring.npow filter.germ.ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_ring.le filter.germ.ordered_ring, lt := ordered_ring.lt filter.germ.ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _, mul_comm := _}

source

@[protected, instance]

def filter.germ.strict_ordered_semiring {α : Type u} {β : Type v} {φ : ultrafilter α} [strict_ordered_semiring β] :

strict_ordered_semiring (↑φ.germ β)

Equations

filter.germ.strict_ordered_semiring = {add := ordered_semiring.add filter.germ.ordered_semiring, add_assoc := _, zero := ordered_semiring.zero filter.germ.ordered_semiring, zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul filter.germ.ordered_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_semiring.mul filter.germ.ordered_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ordered_semiring.one filter.germ.ordered_semiring, one_mul := _, mul_one := _, nat_cast := ordered_semiring.nat_cast filter.germ.ordered_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := ordered_semiring.npow filter.germ.ordered_semiring, npow_zero' := _, npow_succ' := _, le := ordered_semiring.le filter.germ.ordered_semiring, lt := ordered_semiring.lt filter.germ.ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}

source

@[protected, instance]

def filter.germ.strict_ordered_comm_semiring {α : Type u} {β : Type v} {φ : ultrafilter α} [strict_ordered_comm_semiring β] :

strict_ordered_comm_semiring (↑φ.germ β)

Equations

filter.germ.strict_ordered_comm_semiring = {add := strict_ordered_semiring.add filter.germ.strict_ordered_semiring, add_assoc := _, zero := strict_ordered_semiring.zero filter.germ.strict_ordered_semiring, zero_add := _, add_zero := _, nsmul := strict_ordered_semiring.nsmul filter.germ.strict_ordered_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_semiring.mul filter.germ.strict_ordered_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_semiring.one filter.germ.strict_ordered_semiring, one_mul := _, mul_one := _, nat_cast := strict_ordered_semiring.nat_cast filter.germ.strict_ordered_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_semiring.npow filter.germ.strict_ordered_semiring, npow_zero' := _, npow_succ' := _, le := strict_ordered_semiring.le filter.germ.strict_ordered_semiring, lt := strict_ordered_semiring.lt filter.germ.strict_ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}

source

@[protected, instance]

def filter.germ.strict_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [strict_ordered_ring β] :

strict_ordered_ring (↑φ.germ β)

Equations

filter.germ.strict_ordered_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_semiring.le filter.germ.strict_ordered_semiring, lt := strict_ordered_semiring.lt filter.germ.strict_ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _}

source

@[protected, instance]

def filter.germ.strict_ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [strict_ordered_comm_ring β] :

strict_ordered_comm_ring (↑φ.germ β)

Equations

filter.germ.strict_ordered_comm_ring = {add := strict_ordered_ring.add filter.germ.strict_ordered_ring, add_assoc := _, zero := strict_ordered_ring.zero filter.germ.strict_ordered_ring, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul filter.germ.strict_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg filter.germ.strict_ordered_ring, sub := strict_ordered_ring.sub filter.germ.strict_ordered_ring, sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul filter.germ.strict_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast filter.germ.strict_ordered_ring, nat_cast := strict_ordered_ring.nat_cast filter.germ.strict_ordered_ring, one := strict_ordered_ring.one filter.germ.strict_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul filter.germ.strict_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow filter.germ.strict_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le filter.germ.strict_ordered_ring, lt := strict_ordered_ring.lt filter.germ.strict_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, mul_comm := _}

source

@[protected, instance]

noncomputable def filter.germ.linear_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_ring β] :

linear_ordered_ring (↑φ.germ β)

Equations

filter.germ.linear_ordered_ring = {add := strict_ordered_ring.add filter.germ.strict_ordered_ring, add_assoc := _, zero := strict_ordered_ring.zero filter.germ.strict_ordered_ring, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul filter.germ.strict_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg filter.germ.strict_ordered_ring, sub := strict_ordered_ring.sub filter.germ.strict_ordered_ring, sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul filter.germ.strict_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast filter.germ.strict_ordered_ring, nat_cast := strict_ordered_ring.nat_cast filter.germ.strict_ordered_ring, one := strict_ordered_ring.one filter.germ.strict_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul filter.germ.strict_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow filter.germ.strict_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le filter.germ.strict_ordered_ring, lt := strict_ordered_ring.lt filter.germ.strict_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le filter.germ.linear_order, decidable_eq := linear_order.decidable_eq filter.germ.linear_order, decidable_lt := linear_order.decidable_lt filter.germ.linear_order, max := linear_order.max filter.germ.linear_order, max_def := _, min := linear_order.min filter.germ.linear_order, min_def := _}

source

@[protected, instance]

noncomputable def filter.germ.linear_ordered_field {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_field β] :

linear_ordered_field (↑φ.germ β)

Equations

filter.germ.linear_ordered_field = {add := linear_ordered_ring.add filter.germ.linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero filter.germ.linear_ordered_ring, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul filter.germ.linear_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg filter.germ.linear_ordered_ring, sub := linear_ordered_ring.sub filter.germ.linear_ordered_ring, sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul filter.germ.linear_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_ring.int_cast filter.germ.linear_ordered_ring, nat_cast := linear_ordered_ring.nat_cast filter.germ.linear_ordered_ring, one := linear_ordered_ring.one filter.germ.linear_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_ring.mul filter.germ.linear_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow filter.germ.linear_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le filter.germ.linear_ordered_ring, lt := linear_ordered_ring.lt filter.germ.linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le filter.germ.linear_ordered_ring, decidable_eq := linear_ordered_ring.decidable_eq filter.germ.linear_ordered_ring, decidable_lt := linear_ordered_ring.decidable_lt filter.germ.linear_ordered_ring, max := linear_ordered_ring.max filter.germ.linear_ordered_ring, max_def := _, min := linear_ordered_ring.min filter.germ.linear_ordered_ring, min_def := _, mul_comm := _, inv := field.inv filter.germ.field, div := field.div filter.germ.field, div_eq_mul_inv := _, zpow := field.zpow filter.germ.field, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, rat_cast := field.rat_cast filter.germ.field, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul filter.germ.field, qsmul_eq_mul' := _}

source

@[protected, instance]

noncomputable def filter.germ.linear_ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_comm_ring β] :

linear_ordered_comm_ring (↑φ.germ β)

Equations

filter.germ.linear_ordered_comm_ring = {add := linear_ordered_ring.add filter.germ.linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero filter.germ.linear_ordered_ring, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul filter.germ.linear_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg filter.germ.linear_ordered_ring, sub := linear_ordered_ring.sub filter.germ.linear_ordered_ring, sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul filter.germ.linear_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_ring.int_cast filter.germ.linear_ordered_ring, nat_cast := linear_ordered_ring.nat_cast filter.germ.linear_ordered_ring, one := linear_ordered_ring.one filter.germ.linear_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_ring.mul filter.germ.linear_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow filter.germ.linear_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le filter.germ.linear_ordered_ring, lt := linear_ordered_ring.lt filter.germ.linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le filter.germ.linear_ordered_ring, decidable_eq := linear_ordered_ring.decidable_eq filter.germ.linear_ordered_ring, decidable_lt := linear_ordered_ring.decidable_lt filter.germ.linear_ordered_ring, max := linear_ordered_ring.max filter.germ.linear_ordered_ring, max_def := _, min := linear_ordered_ring.min filter.germ.linear_ordered_ring, min_def := _, mul_comm := _}

source

theorem filter.germ.max_def {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : ↑φ.germ β) :

linear_order.max x y = filter.germ.map₂ linear_order.max x y

source

theorem filter.germ.min_def {α : Type u} {β : Type v} {φ : ultrafilter α} [K : linear_order β] (x y : ↑φ.germ β) :

linear_order.min x y = filter.germ.map₂ linear_order.min x y

source

theorem filter.germ.abs_def {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] (x : ↑φ.germ β) :

|x| = filter.germ.map has_abs.abs x

source

@[simp]

theorem filter.germ.const_max {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :

↑(linear_order.max x y) = linear_order.max ↑x ↑y

source

@[simp]

theorem filter.germ.const_min {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :

↑(linear_order.min x y) = linear_order.min ↑x ↑y

source

@[simp]

theorem filter.germ.const_abs {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] (x : β) :

↑|x| = |↑x|

mathlib documentation

Ultraproducts #

Tags #