[Merged by Bors] - feat(order/complete_lattice): add equiv.supr_congr and equiv.supr_comp lemmas

[j-loreaux]

Adds these lemmas as easy consequences of the function.surjective versions in order to aid in discovery.

---

[eric-wieser]

Isn't this a weaker version of function.surjective.supr_congr?

[eric-wieser]

Yes, it is:

Suggested change

	lemma equiv.csupr {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_above (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨆ i, f i) = ⨆ i, g i :=
	begin
	casesI is_empty_or_nonempty ι,
	{ haveI : is_empty ι' := (equiv.is_empty_congr e).mp h, simp only [supr, range_eq_empty] },
	{ haveI : nonempty ι' := (equiv.nonempty_congr e).mp h,
	have hg : bdd_above (range g),
	{ obtain ⟨M, hM⟩ := hf, use M, rintros - ⟨i, rfl⟩, refine hM ⟨(e.symm i), _⟩,
	simpa only [equiv.apply_symm_apply] using hfg (e.symm i), },
	refine le_antisymm (csupr_le (λ i, (hfg i).symm ▸ le_csupr hg (e i))) (csupr_le (λ i, _)),
	simpa only [equiv.apply_symm_apply, hfg (e.symm i)] using le_csupr hf (e.symm i) },
	end
	lemma equiv.cinfi {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_below (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨅ i, f i) = ⨅ i, g i :=
	@equiv.csupr αᵒᵈ _ _ _ e _ hf _ hfg
	lemma equiv.csupr {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_above (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨆ i, f i) = ⨆ i, g i :=
	e.surjective.supr_congr _ $ λ i, (hfg i).symm
	lemma equiv.cinfi {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_below (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨅ i, f i) = ⨅ i, g i :=
	@equiv.csupr αᵒᵈ _ _ _ e _ hf _ hfg

[eric-wieser]

It's maybe worth adding an equiv.supr_congr wrapper for e.surjective.supr_congr just to aid with discoverability, but it wouldn't go in this file.

[eric-wieser]

Yes, it is:

Suggested change

	lemma equiv.csupr {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_above (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨆ i, f i) = ⨆ i, g i :=
	begin
	casesI is_empty_or_nonempty ι,
	{ haveI : is_empty ι' := (equiv.is_empty_congr e).mp h, simp only [supr, range_eq_empty] },
	{ haveI : nonempty ι' := (equiv.nonempty_congr e).mp h,
	have hg : bdd_above (range g),
	{ obtain ⟨M, hM⟩ := hf, use M, rintros - ⟨i, rfl⟩, refine hM ⟨(e.symm i), _⟩,
	simpa only [equiv.apply_symm_apply] using hfg (e.symm i), },
	refine le_antisymm (csupr_le (λ i, (hfg i).symm ▸ le_csupr hg (e i))) (csupr_le (λ i, _)),
	simpa only [equiv.apply_symm_apply, hfg (e.symm i)] using le_csupr hf (e.symm i) },
	end
	lemma equiv.cinfi {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_below (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨅ i, f i) = ⨅ i, g i :=
	@equiv.csupr αᵒᵈ _ _ _ e _ hf _ hfg
	lemma equiv.csupr {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_above (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨆ i, f i) = ⨆ i, g i :=
	e.surjective.supr_congr _ $ λ i, (hfg i).symm
	lemma equiv.cinfi {ι ι' : Type*} (e : ι ≃ ι') {f : ι → α} (hf : bdd_below (range f)) {g : ι' → α}
	(hfg : ∀ i, f i = g (e i)) : (⨅ i, f i) = ⨅ i, g i :=
	@equiv.csupr αᵒᵈ _ _ _ e _ hf _ hfg

[j-loreaux]

I've placed these immediately after function.surjective.supr_congr in order/complete_lattice and protected them since there is a supr_congr in the root namespace. I also protected function.surjective.infi_congr because it was not protected before.

[eric-wieser]

bors d+

Make sure to update the PR title and description, since they are no longer accurate.

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

Bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests