Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-21 09:56 f3835fab

View on Github →

feat(*): assorted simple lemmas, simplify some proofs (#1895)

feat(*): assorted simple lemmas, simplify some proofs
+1 lemma, +1 simplified proof

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_lt_of_real_iff_of_nonneg

Modified src/data/real/nnreal.lean

added theorem nnreal.of_real_lt_of_real_iff_of_nonneg

Modified src/data/set/basic.lean

added theorem set.inter_singleton_nonempty

Modified src/data/set/intervals/basic.lean

added theorem set.nonempty_Iio

added theorem set.nonempty_Ioi

Modified src/order/basic.lean

added theorem directed.mono_comp

Modified src/order/bounded_lattice.lean

added theorem with_top.dense_coe

Modified src/order/filter/basic.lean

added theorem filter.forall_sets_nonempty_iff_ne_bot

Modified src/topology/basic.lean

Modified src/topology/continuous_on.lean

Modified src/topology/sequences.lean