filter.bigly_equal

Two sequences are bigly equal iff the kernel of their difference is in φ

filter.filterprod

Ultraproduct, but on a general filter

filter.filter_product.of

Equivalence class containing the constant sequence of a term in β

filter.filter_product.lift

Lift function to filter product

filter.filter_product.lift₂

Lift binary operation to filter product

filter.filter_product.lift_rel

Lift properties to filter product

filter.filter_product.lift_rel₂

Lift binary relations to filter product