Commit 2024-07-05 17:45 fd7e4ded

View on Github →

feat: make discrete_of_t1_of_finite an instance and rename (#14240) Also adds the lemma Set.Finite.continuousOn which seems to be missing.

Estimated changes

Modified Mathlib/NumberTheory/Liouville/Basic.lean

Modified Mathlib/Topology/Algebra/Field.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/Separation.lean

added theorem Set.Finite.continuousOn

deleted theorem discrete_of_t1_of_finite