From 2e8bd34884e5cdfae3068958a003b2c5b660d388 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Fri, 11 Aug 2017 18:14:46 -0400
Subject: [PATCH] add set.range function

`range` is stronger than `f '' univ`, as `f` can be a function from an arbitrary `Sort` instead of `Type`
---
 data/set/basic.lean         | 27 +++++++++++++++++++++++++++
 order/complete_lattice.lean | 24 ++++++++++++++++++++++--
 2 files changed, 49 insertions(+), 2 deletions(-)

diff --git a/data/set/basic.lean b/data/set/basic.lean
index 46aa4c1dc8495..7f0a951a4860b 100644
--- a/data/set/basic.lean
+++ b/data/set/basic.lean
@@ -657,6 +657,33 @@ theorem eq_preimage_subtype_val_iff {p : α → Prop} {s : set (subtype p)} {t :
 
 end preimage
 
+
+section range
+variables {f : ι → α}
+open function
+
+/-- Range of a function.
+
+This function is more flexiable as `f '' univ`, as the image requires that the domain is in Type
+and not an arbitrary Sort. -/
+def range (f : ι → α) : set α := {x | ∃y, f y = x}
+
+lemma mem_range {i : ι} : f i ∈ range f := ⟨i, rfl⟩ 
+
+lemma forall_range_iff {p : α → Prop} : (∀a∈range f, p a) ↔ (∀i, p (f i)) :=
+⟨assume h i, h (f i) mem_range, assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩
+
+lemma range_of_surjective (h : surjective f) : range f = univ :=
+eq_univ_of_univ_subset $ assume x _, h x
+
+@[simp] lemma range_id : range (@id α) = univ := range_of_surjective surjective_id
+
+lemma range_compose {g : α → β} : range (g ∘ f) = g '' range f :=
+subset.antisymm
+  (forall_range_iff.mpr $ assume i, mem_image_of_mem g mem_range)
+  (bounded_forall_image_iff.mpr $ forall_range_iff.mpr $ assume i, mem_range)
+end range
+
 def pairwise_on (s : set α) (r : α → α → Prop) := ∀x ∈ s, ∀y ∈ s, x ≠ y → r x y
 
 end set
diff --git a/order/complete_lattice.lean b/order/complete_lattice.lean
index ea5908d9373e4..0f44ea3a86083 100644
--- a/order/complete_lattice.lean
+++ b/order/complete_lattice.lean
@@ -385,14 +385,34 @@ le_antisymm
   (Sup_le $ assume b h, le_supr_of_le b $ le_supr _ h)
   (supr_le $ assume b, supr_le $ assume h, le_Sup h)
 
-theorem Inf_image {s : set β} {f : β → α} : Inf (set.image f s) = (⨅ a ∈ s, f a) :=
+lemma Sup_range {f : ι → α} : Sup (range f) = supr f :=
+le_antisymm
+  (Sup_le $ forall_range_iff.mpr $ assume i, le_supr _ _)
+  (supr_le $ assume i, le_Sup mem_range)
+
+lemma Inf_range {f : ι → α} : Inf (range f) = infi f :=
+le_antisymm
+  (le_infi $ assume i, Inf_le mem_range)
+  (le_Inf $ forall_range_iff.mpr $ assume i, infi_le _ _)
+
+lemma supr_range {g : β → α} {f : ι → β} : (⨆b∈range f, g b) = (⨆i, g (f i)) :=
+le_antisymm
+  (supr_le $ assume b, supr_le $ assume ⟨i, (h : f i = b)⟩, h ▸ le_supr _ i)
+  (supr_le $ assume i, le_supr_of_le (f i) $ le_supr (λp, g (f i)) mem_range)
+
+lemma infi_range {g : β → α} {f : ι → β} : (⨅b∈range f, g b) = (⨅i, g (f i)) :=
+le_antisymm
+  (le_infi $ assume i, infi_le_of_le (f i) $ infi_le (λp, g (f i)) mem_range)
+  (le_infi $ assume b, le_infi $ assume ⟨i, (h : f i = b)⟩, h ▸ infi_le _ i)
+
+theorem Inf_image {s : set β} {f : β → α} : Inf (f '' s) = (⨅ a ∈ s, f a) :=
 calc Inf (set.image f s) = (⨅a, ⨅h : ∃b, b ∈ s ∧ f b = a, a) : Inf_eq_infi
                      ... = (⨅a, ⨅b, ⨅h : f b = a ∧ b ∈ s, a) : by simp
                      ... = (⨅a, ⨅b, ⨅h : a = f b, ⨅h : b ∈ s, a) : by simp [infi_and, eq_comm]
                      ... = (⨅b, ⨅a, ⨅h : a = f b, ⨅h : b ∈ s, a) : by rw [infi_comm]
                      ... = (⨅a∈s, f a) : congr_arg infi $ funext $ assume x, by rw [infi_infi_eq_left]
 
-theorem Sup_image {s : set β} {f : β → α} : Sup (set.image f s) = (⨆ a ∈ s, f a) :=
+theorem Sup_image {s : set β} {f : β → α} : Sup (f '' s) = (⨆ a ∈ s, f a) :=
 calc Sup (set.image f s) = (⨆a, ⨆h : ∃b, b ∈ s ∧ f b = a, a) : Sup_eq_supr
                      ... = (⨆a, ⨆b, ⨆h : f b = a ∧ b ∈ s, a) : by simp
                      ... = (⨆a, ⨆b, ⨆h : a = f b, ⨆h : b ∈ s, a) : by simp [supr_and, eq_comm]