Commit 2024-06-17 10:24 217718fb

View on Github →

feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual (#13642)

Estimated changes

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.eval_image_pi_of_not_mem

Modified Mathlib/Order/Basic.lean

added theorem Prod.mk_lt_mk_of_le_of_lt

added theorem Prod.mk_lt_mk_of_lt_of_le

Modified Mathlib/Topology/Bases.lean

added theorem isOpenMap_eval

Modified Mathlib/Topology/Basic.lean

added theorem nhdsWithin_neBot

Modified Mathlib/Topology/Constructions.lean