Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-05 09:22 7f208430

View on Github →

chore(order/filter): rephrase filter.has_le (#1399) The goal of this tiny refactor is to prevent filter.sets leaking when proving a filter g is finer than another one f. We want the goal to be s ∈ f → s ∈ g instead of the definitionaly equivalent s ∈ f.sets ∈ g.sets

Estimated changes