Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-11 18:14 2e8bd348

View on Github →

add set.range function range is stronger than f '' univ, as f can be a function from an arbitrary Sort instead of Type

Estimated changes

Modified data/set/basic.lean

added theorem set.forall_range_iff

added theorem set.mem_range

added def set.range

added theorem set.range_compose

added theorem set.range_id

added theorem set.range_of_surjective

Modified order/complete_lattice.lean

modified theorem lattice.Inf_image

added theorem lattice.Inf_range

modified theorem lattice.Sup_image

added theorem lattice.Sup_range

added theorem lattice.infi_range

added theorem lattice.supr_range