Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-26 15:16 034cf668

View on Github →

chore(set_theory/ordinal/topology): add variables block (#14369) We rename a bunch of variables, but don't fundamentally change any proof.

Estimated changes

Modified src/set_theory/ordinal/topology.lean

modified theorem ordinal.enum_ord_is_normal_iff_is_closed

modified theorem ordinal.is_closed_iff_bsup

modified theorem ordinal.is_closed_iff_sup

modified theorem ordinal.is_limit_of_mem_frontier

modified theorem ordinal.is_open_iff

modified theorem ordinal.is_open_singleton_iff

modified theorem ordinal.mem_closed_iff_bsup

modified theorem ordinal.mem_closed_iff_sup

modified theorem ordinal.mem_closure_iff_bsup

modified theorem ordinal.mem_closure_iff_sup