Pointwise operations on sets of reals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file relates
Inf (a • s)/
Sup (a • s) with
a • Inf s/
a • Sup s for
s : set ℝ.
From these, it relates
⨅ i, a • f i /
⨆ i, a • f i with
a • (⨅ i, f i) /
a • (⨆ i, f i),
and provides lemmas about distributing
This is true more generally for conditionally complete linear order whose default value is
don't have those yet.
Special cases for real multiplication #