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_nonneg
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[Zero M]
{s : Set α}
{f : α → M}
(h : ∀ a ∈ s, 0 ≤ f a)
(a : α)
:
0 ≤ Set.indicator s f a
theorem
Set.one_le_mulIndicator
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[One M]
{s : Set α}
{f : α → M}
(h : ∀ a ∈ s, 1 ≤ f a)
(a : α)
:
1 ≤ Set.mulIndicator s f a
theorem
Set.indicator_nonpos
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[Zero M]
{s : Set α}
{f : α → M}
(h : ∀ a ∈ s, f a ≤ 0)
(a : α)
:
Set.indicator s f a ≤ 0
theorem
Set.mulIndicator_le_one
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[One M]
{s : Set α}
{f : α → M}
(h : ∀ a ∈ s, f a ≤ 1)
(a : α)
:
Set.mulIndicator s f a ≤ 1
theorem
Set.indicator_le_indicator
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[Zero M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
(h : f a ≤ g a)
:
Set.indicator s f a ≤ Set.indicator s g a
theorem
Set.mulIndicator_le_mulIndicator
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[One M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
(h : f a ≤ g a)
:
Set.mulIndicator s f a ≤ Set.mulIndicator s g a
theorem
Set.indicator_le_indicator_of_subset
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[Zero M]
{s : Set α}
{t : Set α}
{f : α → M}
(h : s ⊆ t)
(hf : ∀ (a : α), 0 ≤ f a)
(a : α)
:
Set.indicator s f a ≤ Set.indicator t f a
theorem
Set.mulIndicator_le_mulIndicator_of_subset
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[One M]
{s : Set α}
{t : Set α}
{f : α → M}
(h : s ⊆ t)
(hf : ∀ (a : α), 1 ≤ f a)
(a : α)
:
Set.mulIndicator s f a ≤ Set.mulIndicator t f a
theorem
Set.indicator_le_self'
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[Zero M]
{s : Set α}
{f : α → M}
(hf : ∀ x ∉ s, 0 ≤ f x)
:
Set.indicator s f ≤ f
theorem
Set.mulIndicator_le_self'
{α : Type u_2}
{M : Type u_4}
[Preorder M]
[One M]
{s : Set α}
{f : α → M}
(hf : ∀ x ∉ s, 1 ≤ f x)
:
Set.mulIndicator s f ≤ f
theorem
Set.indicator_le_indicator_nonneg
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(s : Set α)
(f : α → M)
:
Set.indicator s f ≤ Set.indicator {a : α | 0 ≤ f a} f
theorem
Set.indicator_nonpos_le_indicator
{α : Type u_2}
{M : Type u_4}
[Zero M]
[LinearOrder M]
(s : Set α)
(f : α → M)
:
Set.indicator {a : α | f a ≤ 0} f ≤ Set.indicator s f
theorem
Set.indicator_iUnion_apply
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[Zero M]
(h1 : ⊥ = 0)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.indicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), Set.indicator (s i) f x
theorem
Set.mulIndicator_iUnion_apply
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[One M]
(h1 : ⊥ = 1)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), Set.mulIndicator (s i) f x
theorem
Set.indicator_iInter_apply
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[Zero M]
[Nonempty ι]
(h1 : ⊥ = 0)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.indicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), Set.indicator (s i) f x
theorem
Set.mulIndicator_iInter_apply
{ι : Sort u_1}
{α : Type u_2}
{M : Type u_4}
[CompleteLattice M]
[One M]
[Nonempty ι]
(h1 : ⊥ = 1)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), Set.mulIndicator (s i) f x
theorem
Set.indicator_le_self
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedAddCommMonoid M]
(s : Set α)
(f : α → M)
:
Set.indicator s f ≤ f
theorem
Set.mulIndicator_le_self
{α : Type u_2}
{M : Type u_4}
[CanonicallyOrderedCommMonoid M]
(s : Set α)
(f : α → M)
:
Set.mulIndicator s 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)
:
Set.indicator s 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)
:
Set.mulIndicator s 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)
:
Set.indicator s 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)
:
Set.mulIndicator s f ≤ g
theorem
Set.abs_indicator_symmDiff
{α : Type u_2}
{M : Type u_4}
[LinearOrderedAddCommGroup M]
(s : Set α)
(t : Set α)
(f : α → M)
(x : α)
:
|Set.indicator (s ∆ t) f x| = |Set.indicator s f x - Set.indicator t f x|