feat(*): add a few lemmas about function.extend (#11498)

I'm going to use `function.extend` as another way to get from
`[encodable ι] (s : ι → set α)` to `t : ℕ → set α` in measure theory.

src/logic/function/basic.lean

@@ -526,6 +526,15 @@ end
   extend f g e' b = e' b :=
 by simp [function.extend_def, hb]
 
+lemma apply_extend {δ} (hf : injective f) (F : γ → δ) (g : α → γ) (e' : β → γ) (b : β) :
+  F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
+begin
+  by_cases hb : ∃ a, f a = b,
+  { cases hb with a ha, subst b,
+    rw [extend_apply hf, extend_apply hf] },
+  { rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb] }
+end
+
 lemma extend_injective (hf : injective f) (e' : β → γ) :
   injective (λ g, extend f g e') :=
 begin

src/order/complete_lattice.lean

@@ -32,7 +32,7 @@ also use `bsupr`/`binfi` for "bounded" supremum or infimum, i.e. one of `⨆ i 
 -/
 
 set_option old_structure_cmd true
-open set
+open set function
 
 variables {α β β₂ : Type*} {ι ι₂ : Sort*}
 
@@ -530,12 +530,12 @@ lemma monotone.supr_comp_eq [preorder β] {f : β → α} (hf : monotone f)
 le_antisymm (supr_comp_le _ _) (supr_le_supr2 $ λ x, (hs x).imp $ λ i hi, hf hi)
 
 lemma function.surjective.supr_comp {α : Type*} [has_Sup α] {f : ι → ι₂}
-  (hf : function.surjective f) (g : ι₂ → α) :
+  (hf : surjective f) (g : ι₂ → α) :
   (⨆ x, g (f x)) = ⨆ y, g y :=
 by simp only [supr, hf.range_comp]
 
 lemma supr_congr {α : Type*} [has_Sup α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂)
-  (h1 : function.surjective h) (h2 : ∀ x, g (h x) = f x) : (⨆ x, f x) = ⨆ y, g y :=
+  (h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⨆ x, f x) = ⨆ y, g y :=
 by { convert h1.supr_comp g, exact (funext h2).symm }
 
 -- TODO: finish doesn't do well here.
@@ -627,12 +627,12 @@ lemma monotone.infi_comp_eq [preorder β] {f : β → α} (hf : monotone f)
 le_antisymm (infi_le_infi2 $ λ x, (hs x).imp $ λ i hi, hf hi) (le_infi_comp _ _)
 
 lemma function.surjective.infi_comp {α : Type*} [has_Inf α] {f : ι → ι₂}
-  (hf : function.surjective f) (g : ι₂ → α) :
+  (hf : surjective f) (g : ι₂ → α) :
   (⨅ x, g (f x)) = ⨅ y, g y :=
 @function.surjective.supr_comp _ _ (order_dual α) _ f hf g
 
 lemma infi_congr {α : Type*} [has_Inf α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂)
-  (h1 : function.surjective h) (h2 : ∀ x, g (h x) = f x) : (⨅ x, f x) = ⨅ y, g y :=
+  (h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⨅ x, f x) = ⨅ y, g y :=
 @supr_congr _ _ (order_dual α) _ _ _ h h1 h2
 
 @[congr] theorem infi_congr_Prop {α : Type*} [has_Inf α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
@@ -999,6 +999,14 @@ lemma supr_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
   (⨆ c ∈ f '' t, g c) = (⨆ b ∈ t, g (f b)) :=
 @infi_image (order_dual α) _ _ _ _ _ _
 
+theorem supr_extend_bot {e : ι → β} (he : injective e) (f : ι → α) :
+  (⨆ j, extend e f ⊥ j) = ⨆ i, f i :=
+begin
+  rw supr_split _ (λ j, ∃ i, e i = j),
+  simp [extend_apply he, extend_apply', @supr_comm _ β ι] { contextual := tt }
+end
+
+
 /-!
 ### `supr` and `infi` under `Type`
 -/

src/order/directed.lean

@@ -72,6 +72,20 @@ lemma monotone.directed_le [semilattice_sup α] [preorder β] {f : α → β} :
   monotone f → directed (≤) f :=
 directed_of_sup
 
+lemma directed.extend_bot [preorder α] [order_bot α] {e : ι → β} {f : ι → α}
+  (hf : directed (≤) f) (he : function.injective e) :
+  directed (≤) (function.extend e f ⊥) :=
+begin
+  intros a b,
+  rcases (em (∃ i, e i = a)).symm with ha | ⟨i, rfl⟩,
+  { use b, simp [function.extend_apply' _ _ _ ha] },
+  rcases (em (∃ i, e i = b)).symm with hb | ⟨j, rfl⟩,
+  { use e i, simp [function.extend_apply' _ _ _ hb] },
+  rcases hf i j with ⟨k, hi, hj⟩,
+  use (e k),
+  simp only [function.extend_apply he, *, true_and]
+end
+
 /-- An antitone function on an inf-semilattice is directed. -/
 lemma directed_of_inf [semilattice_inf α] {r : β → β → Prop} {f : α → β}
   (hf : ∀ a₁ a₂, a₁ ≤ a₂ → r (f a₂) (f a₁)) : directed r f :=