Def Filter.pureOneHom

Modification history

2023-09-12 12:40

Mathlib/Order/Filter/Pointwise.lean

chore: replace anonymous morphism constructors with named fields (#7015) …

Modified Filter.pureOneHom View on Github →

2023-01-30 19:30

Mathlib/Order/Filter/Pointwise.lean

feat: port Order.Filter.Pointwise (#1839)

Added Filter.pureOneHom View on Github →