Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-22 14:57 7dff92aa

View on Github →

feat(category_theory/morphism_property): Define morphism_property.universally. (#17112)

Estimated changes

Modified src/category_theory/morphism_property.lean

added theorem category_theory.morphism_property.stable_under_base_change.universally_eq

added theorem category_theory.morphism_property.stable_under_composition.universally

added def category_theory.morphism_property.universally

added theorem category_theory.morphism_property.universally_le

added theorem category_theory.morphism_property.universally_mono

added theorem category_theory.morphism_property.universally_respects_iso

added theorem category_theory.morphism_property.universally_stable_under_base_change