Commit 2024-05-27 06:08 600c344d

View on Github →

chore: mv principal_subtype (#13232)

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.principal_subtype

Modified Mathlib/Topology/ContinuousOn.lean

deleted theorem principal_subtype