Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 03:47 3ec54df5

View on Github →

feat(data/finset/lattice): le_sup_iff and lt_sup_iff (#7182) A few changes and additions to finset/lattice in response to this Zulip thread https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/finset.2Esup'

Estimated changes

modified theorem finset.exists_mem_eq_inf
modified theorem finset.exists_mem_eq_sup
added theorem finset.inf'_induction
added theorem finset.inf'_le_iff
added theorem finset.inf'_lt_iff
added theorem finset.inf_induction
added theorem finset.inf_le_iff
added theorem finset.inf_lt_iff
added theorem finset.le_sup'_iff
added theorem finset.le_sup_iff
modified theorem finset.lt_inf_iff
added theorem finset.lt_sup'_iff
added theorem finset.lt_sup_iff
deleted theorem finset.of_inf'_of_forall
deleted theorem finset.of_inf_of_forall
deleted theorem finset.of_sup'_of_forall
deleted theorem finset.of_sup_of_forall
added theorem finset.sup'_induction
added theorem finset.sup_induction