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.iSup_indicator
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[Zero M]
{ι : Type u_5}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{f : ι → α → M}
{s : ι → Set α}
(h1 : ⊥ = 0)
(hf : Monotone f)
(hs : Monotone s)
:
⨆ (i : ι), (s i).indicator (f i) = (⋃ (i : ι), s i).indicator (⨆ (i : ι), f i)
theorem
Set.iSup_mulIndicator
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[One M]
{ι : Type u_5}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{f : ι → α → M}
{s : ι → Set α}
(h1 : ⊥ = 1)
(hf : Monotone f)
(hs : Monotone s)
:
⨆ (i : ι), (s i).mulIndicator (f i) = (⋃ (i : ι), s i).mulIndicator (⨆ (i : ι), f i)
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 : α)
: