chore(Order/Filter/IsBounded): use to_dual

[JovanGerb]

use to_dual for Filter.IsBounded

---

• depends on: chore(Order/Filter/AtTopBot/Basic): use to_dual #37747

[github-actions]

PR summary fcdb939818

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- Antitone.frequently_ge_map_of_frequently_le
- Antitone.isBoundedUnder_ge_comp_iff
- Antitone.isCoboundedUnder_ge_of_isCobounded
- Eventually.exists_forall_of_atBot
- Finite.bddBelow
- Finite.bddBelow_biUnion
- IsBounded.isCobounded_ge
- IsBoundedUnder.bddBelow_range
- IsBoundedUnder.bddBelow_range_of_cofinite
- IsBoundedUnder.eventually_ge
- IsBoundedUnder.ge_of_finite
- IsBoundedUnder.inf
- IsBoundedUnder.isCoboundedUnder_ge
- IsBoundedUnder.mono_ge
- IsCobounded.frequently_le
- IsCobounded.of_frequently_le
- IsCoboundedUnder.frequently_le
- IsCoboundedUnder.of_frequently_le
- Monotone.frequently_le_map_of_frequently_le
- Monotone.isBoundedUnder_ge_comp_iff
- Monotone.isCoboundedUnder_ge_of_isCobounded
- Tendsto.isBoundedUnder_ge_atTop
- _root_.Antitone.isBoundedUnder_ge_comp
- _root_.BddBelow.isBoundedUnder
- _root_.BddBelow.isBoundedUnder_of_range
- _root_.Monotone.isBoundedUnder_ge_comp
- _root_.OrderIso.isBoundedUnder_ge_comp
- atBot_Iic_eq
- atBot_Iio_eq
- atBot_basis'
- atBot_basis_Iio
- atBot_basis_Iio'
- atBot_neBot
- atBot_neBot_iff
- bddBelow
- eventually_atBot
- exists_le_of_tendsto_atBot
- exists_lt_of_tendsto_atBot
- frequently_atBot
- frequently_atBot'
- inf_map_atBot_neBot_iff
- infinite_of_not_bddBelow
- isBoundedUnder_ge_add
- isBoundedUnder_ge_inf
- isBoundedUnder_ge_sum
- isBoundedUnder_iff_eventually_bddBelow
- isBoundedUnder_of_eventually_ge
- isBounded_ge_atTop
- isBounded_ge_of_bot
- isCoboundedUnder_ge_add
- isCoboundedUnder_ge_of_eventually_le
- isCoboundedUnder_ge_of_le
- isCobounded_ge_of_top
- map_atBot_eq
- map_atBot_eq_of_gc
- map_atBot_eq_of_gc_preorder
- map_val_Iic_atBot
- map_val_Iio_atBot
- mem_atBot_sets
- not_bddBelow_of_tendsto_atBot
- not_isBoundedUnder_of_tendsto_atBot
- tendsto_Iic_atBot
- tendsto_Iio_atBot
- tendsto_atBot'
- tendsto_atBot_atBot
- tendsto_atBot_atBot_iff_of_monotone
- tendsto_atBot_atTop
- tendsto_atBot_atTop_iff_of_antitone
- tendsto_atBot_principal
- tendsto_comp_val_Iic_atBot
- tendsto_comp_val_Iio_atBot

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
6783	-3	backward.isDefEq.respectTransparency

Current commit 9258e4ebad
Reference commit fcdb939818

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Order/Filter/AtTopBot/Basic): use to_dual #37747
  By Dependent Issues (🤖). Happy coding!