Commit 2024-03-14 10:04 af0f54a9

View on Github →

chore: replace λ by fun (#11301) Per the style guidelines, λ is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes

  • In lines I was modifying anyway, I also converted => to ↦.
  • Also contains some mild in-passing indentation fixes in Mathlib/Order/SupClosed.
  • Some doc comments still contained Lean 3 syntax λ x, , which I also replaced.
<!-- The text above the `

Estimated changes

modified theorem Fintype.one_le_prod
modified theorem Fintype.prod_le_one
modified theorem Nat.tendsto_div_const_atTop
modified theorem SimpleGraph.isAcyclic_bot
modified theorem Rel.comp_left_top
modified theorem Rel.comp_right_top
modified theorem Set.subset_infs_self
modified theorem Set.subset_sups_self
modified def EmptyRelation
modified theorem Equivalence.symmetric
modified theorem IsLowerSet.infClosed
modified def Foo2.Simps.elim
modified def another_term
modified def baz
modified def foo.rfl3
modified def some_test1
modified def thing