Support of a function in an order #
This file relates the support of a function to order constructions.
theorem
Function.support_sup
{α : Type u_2}
{M : Type u_4}
[Zero M]
[SemilatticeSup M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => f x ⊔ g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_sup
{α : Type u_2}
{M : Type u_4}
[One M]
[SemilatticeSup M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun (x : α) => f x ⊔ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_inf
{α : Type u_2}
{M : Type u_4}
[Zero M]
[SemilatticeInf M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => f x ⊓ g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_inf
{α : Type u_2}
{M : Type u_4}
[One M]
[SemilatticeInf M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun (x : α) => f x ⊓ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_max
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => max (f x) (g x)) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_max
{α : Type u_2}
{M : Type u_4}
[One M]
[LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun (x : α) => max (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_min
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => min (f x) (g x)) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_min
{α : Type u_2}
{M : Type u_4}
[One M]
[LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun (x : α) => min (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_iSup
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[Zero M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.support fun (x : α) => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.support (f i)
theorem
Function.mulSupport_iSup
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[One M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun (x : α) => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.mulSupport (f i)
theorem
Function.support_iInf
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[Zero M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.support fun (x : α) => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.support (f i)
theorem
Function.mulSupport_iInf
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[One M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun (x : α) => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.mulSupport (f i)
theorem
Set.indicator_le_indicator_nonneg
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(s : Set α)
(f : α → M)
:
theorem
Set.indicator_nonpos_le_indicator
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(s : Set α)
(f : α → M)
:
theorem
Set.indicator_le_self
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedAddCommMonoid M]
(s : Set α)
(f : α → M)
:
s.indicator f ≤ f
theorem
Set.mulIndicator_le_self
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedCommMonoid M]
(s : Set α)
(f : α → M)
:
s.mulIndicator f ≤ f
theorem
Set.indicator_apply_le
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedAddCommMonoid M]
{a : α}
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : a ∈ s → f a ≤ g a)
:
s.indicator f a ≤ g a
theorem
Set.mulIndicator_apply_le
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedCommMonoid M]
{a : α}
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : a ∈ s → f a ≤ g a)
:
s.mulIndicator f a ≤ g a
theorem
Set.indicator_le
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedAddCommMonoid M]
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : ∀ a ∈ s, f a ≤ g a)
:
s.indicator f ≤ g
theorem
Set.mulIndicator_le
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedCommMonoid M]
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : ∀ a ∈ s, f a ≤ g a)
:
s.mulIndicator f ≤ g
theorem
Set.abs_indicator_symmDiff
{α : Type u_2}
{M : Type u_4}
[LinearOrderedAddCommGroup M]
(s : Set α)
(t : Set α)
(f : α → M)
(x : α)
: