Zulip Chat Archive

Stream: mathlib4

Topic: New dot lemmas

Yury G. Kudryashov (Feb 06 2023 at 16:51):

Should we rename/alias lemmas like isOpen_empty to IsOpen.empty so that they can be used as .empty?

Yury G. Kudryashov (Feb 06 2023 at 17:11):

MeasurableSet had these lemmas in Lean 3. I'm porting measurable_space_def now, and it's nice to be able to write .unionᵢ fun x => _

Last updated: May 02 2025 at 03:31 UTC