Commit 2023-02-27 11:23 5107462b

View on Github →

feat: port CategoryTheory.Filtered (#2493)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Filtered.lean

added theorem CategoryTheory.Functor.ranges_directed

added theorem CategoryTheory.IsCofiltered.cone_nonempty

added theorem CategoryTheory.IsCofiltered.cospan

added theorem CategoryTheory.IsCofiltered.eq_condition

added theorem CategoryTheory.IsCofiltered.infTo_commutes

added theorem CategoryTheory.IsCofiltered.inf_exists

added theorem CategoryTheory.IsCofiltered.inf_objs_exists

added theorem CategoryTheory.IsCofiltered.of_equivalence

added theorem CategoryTheory.IsCofiltered.of_isLeftAdjoint

added theorem CategoryTheory.IsCofiltered.of_left_adjoint

added theorem CategoryTheory.IsFiltered.bowtie

added theorem CategoryTheory.IsFiltered.cocone_nonempty

added theorem CategoryTheory.IsFiltered.coeq_condition

added theorem CategoryTheory.IsFiltered.coeq₃_condition₁

added theorem CategoryTheory.IsFiltered.coeq₃_condition₂

added theorem CategoryTheory.IsFiltered.coeq₃_condition₃

added theorem CategoryTheory.IsFiltered.of_equivalence

added theorem CategoryTheory.IsFiltered.of_isRightAdjoint

added theorem CategoryTheory.IsFiltered.of_right_adjoint

added theorem CategoryTheory.IsFiltered.span

added theorem CategoryTheory.IsFiltered.sup_exists

added theorem CategoryTheory.IsFiltered.sup_objs_exists

added theorem CategoryTheory.IsFiltered.toSup_commutes

added theorem CategoryTheory.IsFiltered.tulip