Commit 2024-01-25 14:36 fe3b2b22

View on Github →

feat(Data/Sigma): add Sigma.fst_surjective etc (#9914)

Add Sigma.fst_surjective, Sigma.fst_surjective_iff, Sigma.fst_injective, and Sigma.fst_injective_iff.
Move sigma_mk_injective up.
Open Function namespace, drop Function..
Fix indentation.

Estimated changes

Modified Mathlib/Data/Sigma/Basic.lean

added theorem Sigma.fst_injective

added theorem Sigma.fst_injective_iff

added theorem Sigma.fst_surjective

added theorem Sigma.fst_surjective_iff

modified theorem sigma_mk_injective