Def SSet.hornInclusion

Modification history

2025-03-14 12:47
Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean
refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API (#21090) …
Deleted SSet.hornInclusionView on Github →
2025-01-24 19:52
Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
chore(AlgebraicTopology): split SimplicialSet.Basic (#21025) …
Modified SSet.hornInclusionView on Github →
2023-06-19 13:10
Mathlib/AlgebraicTopology/SimplicialSet.lean
chore: add @[ext] lemmas for NatTrans synonyms (#5228)
Modified SSet.hornInclusionView on Github →
2023-04-28 02:53
Mathlib/AlgebraicTopology/SimplicialSet.lean
feat: port AlgebraicTopology.SimplicialSet (#3689)
Added SSet.hornInclusionView on Github →