Support of a function in an order

This file relates the support of a function to order constructions.

theorem Function.mulSupport_sup {α : Type u_2} {M : Type u_3} [One M] [SemilatticeSup M] (f g : α → M) : (mulSupport fun (x : α) => f x ⊔ g x) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_sup {α : Type u_2} {M : Type u_3} [Zero M] [SemilatticeSup M] (f g : α → M) : (support fun (x : α) => f x ⊔ g x) ⊆ support f ∪ support g

theorem Function.mulSupport_inf {α : Type u_2} {M : Type u_3} [One M] [SemilatticeInf M] (f g : α → M) : (mulSupport fun (x : α) => f x ⊓ g x) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_inf {α : Type u_2} {M : Type u_3} [Zero M] [SemilatticeInf M] (f g : α → M) : (support fun (x : α) => f x ⊓ g x) ⊆ support f ∪ support g

theorem Function.mulSupport_max {α : Type u_2} {M : Type u_3} [One M] [LinearOrder M] (f g : α → M) : (mulSupport fun (x : α) => max (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_max {α : Type u_2} {M : Type u_3} [Zero M] [LinearOrder M] (f g : α → M) : (support fun (x : α) => max (f x) (g x)) ⊆ support f ∪ support g

theorem Function.mulSupport_min {α : Type u_2} {M : Type u_3} [One M] [LinearOrder M] (f g : α → M) : (mulSupport fun (x : α) => min (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_min {α : Type u_2} {M : Type u_3} [Zero M] [LinearOrder M] (f g : α → M) : (support fun (x : α) => min (f x) (g x)) ⊆ support f ∪ support g

theorem Function.mulSupport_iSup {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [One M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) : (mulSupport fun (x : α) => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), mulSupport (f i)

theorem Function.support_iSup {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [Zero M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) : (support fun (x : α) => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), support (f i)

theorem Function.mulSupport_iInf {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [One M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) : (mulSupport fun (x : α) => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), mulSupport (f i)

theorem Function.support_iInf {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [Zero M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) : (support fun (x : α) => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), support (f i)

theorem Set.mulIndicator_apply_le' {α : Type u_2} {M : Type u_3} [LE M] [One M] {s : Set α} {f : α → M} {a : α} {y : M} (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) : s.mulIndicator f a ≤ y

theorem Set.indicator_apply_le' {α : Type u_2} {M : Type u_3} [LE M] [Zero M] {s : Set α} {f : α → M} {a : α} {y : M} (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 0 ≤ y) : s.indicator f a ≤ y

theorem Set.mulIndicator_le' {α : Type u_2} {M : Type u_3} [LE M] [One M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a ∉ s, 1 ≤ g a) : s.mulIndicator f ≤ g

theorem Set.indicator_le' {α : Type u_2} {M : Type u_3} [LE M] [Zero M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a ∉ s, 0 ≤ g a) : s.indicator f ≤ g

theorem Set.le_mulIndicator_apply {α : Type u_2} {M : Type u_3} [LE M] [One M] {s : Set α} {g : α → M} {a : α} {y : M} (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 1) : y ≤ s.mulIndicator g a

theorem Set.le_indicator_apply {α : Type u_2} {M : Type u_3} [LE M] [Zero M] {s : Set α} {g : α → M} {a : α} {y : M} (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 0) : y ≤ s.indicator g a

theorem Set.le_mulIndicator {α : Type u_2} {M : Type u_3} [LE M] [One M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 1) : f ≤ s.mulIndicator g

theorem Set.le_indicator {α : Type u_2} {M : Type u_3} [LE M] [Zero M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 0) : f ≤ s.indicator g

theorem Set.one_le_mulIndicator_apply {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f : α → M} {a : α} (h : a ∈ s → 1 ≤ f a) : 1 ≤ s.mulIndicator f a

theorem Set.indicator_apply_nonneg {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f : α → M} {a : α} (h : a ∈ s → 0 ≤ f a) : 0 ≤ s.indicator f a

theorem Set.one_le_mulIndicator {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f : α → M} (h : ∀ a ∈ s, 1 ≤ f a) (a : α) : 1 ≤ s.mulIndicator f a

theorem Set.indicator_nonneg {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f : α → M} (h : ∀ a ∈ s, 0 ≤ f a) (a : α) : 0 ≤ s.indicator f a

theorem Set.mulIndicator_apply_le_one {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f : α → M} {a : α} (h : a ∈ s → f a ≤ 1) : s.mulIndicator f a ≤ 1

theorem Set.indicator_apply_nonpos {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f : α → M} {a : α} (h : a ∈ s → f a ≤ 0) : s.indicator f a ≤ 0

theorem Set.mulIndicator_le_one {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f : α → M} (h : ∀ a ∈ s, f a ≤ 1) (a : α) : s.mulIndicator f a ≤ 1

theorem Set.indicator_nonpos {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f : α → M} (h : ∀ a ∈ s, f a ≤ 0) (a : α) : s.indicator f a ≤ 0

theorem Set.mulIndicator_le_mulIndicator' {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f g : α → M} {a : α} (h : a ∈ s → f a ≤ g a) : s.mulIndicator f a ≤ s.mulIndicator g a

theorem Set.indicator_le_indicator' {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f g : α → M} {a : α} (h : a ∈ s → f a ≤ g a) : s.indicator f a ≤ s.indicator g a

theorem Set.mulIndicator_le_mulIndicator {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f g : α → M} {a : α} (h : f a ≤ g a) : s.mulIndicator f a ≤ s.mulIndicator g a

theorem Set.indicator_le_indicator {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f g : α → M} {a : α} (h : f a ≤ g a) : s.indicator f a ≤ s.indicator g a

theorem Set.mulIndicator_mono {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f g : α → M} (h : f ≤ g) : s.mulIndicator f ≤ s.mulIndicator g

theorem Set.indicator_mono {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f g : α → M} (h : f ≤ g) : s.indicator f ≤ s.indicator g

theorem Set.mulIndicator_le_mulIndicator_apply_of_subset {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s t : Set α} {f : α → M} {a : α} (h : s ⊆ t) (hf : 1 ≤ f a) : s.mulIndicator f a ≤ t.mulIndicator f a

theorem Set.indicator_le_indicator_apply_of_subset {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s t : Set α} {f : α → M} {a : α} (h : s ⊆ t) (hf : 0 ≤ f a) : s.indicator f a ≤ t.indicator f a

theorem Set.mulIndicator_le_mulIndicator_of_subset {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s t : Set α} {f : α → M} (h : s ⊆ t) (hf : 1 ≤ f) : s.mulIndicator f ≤ t.mulIndicator f

theorem Set.indicator_le_indicator_of_subset {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s t : Set α} {f : α → M} (h : s ⊆ t) (hf : 0 ≤ f) : s.indicator f ≤ t.indicator f

theorem Set.mulIndicator_le_self' {α : Type u_2} {M : Type u_3} [Preorder M] [One M] {s : Set α} {f : α → M} (hf : ∀ x ∉ s, 1 ≤ f x) : s.mulIndicator f ≤ f

theorem Set.indicator_le_self' {α : Type u_2} {M : Type u_3} [Preorder M] [Zero M] {s : Set α} {f : α → M} (hf : ∀ x ∉ s, 0 ≤ f x) : s.indicator f ≤ f

theorem Set.indicator_le_indicator_nonneg {α : Type u_2} {M : Type u_3} [Zero M] [LinearOrder M] (s : Set α) (f : α → M) : s.indicator f ≤ {a : α | 0 ≤ f a}.indicator f

theorem Set.indicator_nonpos_le_indicator {α : Type u_2} {M : Type u_3} [Zero M] [LinearOrder M] (s : Set α) (f : α → M) : {a : α | f a ≤ 0}.indicator f ≤ s.indicator f

theorem Set.mulIndicator_iUnion_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [CompleteLattice M] [One M] (h1 : ⊥ = 1) (s : ι → Set α) (f : α → M) (x : α) : (⋃ (i : ι), s i).mulIndicator f x = ⨆ (i : ι), (s i).mulIndicator f x

theorem Set.indicator_iUnion_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [CompleteLattice M] [Zero M] (h1 : ⊥ = 0) (s : ι → Set α) (f : α → M) (x : α) : (⋃ (i : ι), s i).indicator f x = ⨆ (i : ι), (s i).indicator f x

theorem Set.mulIndicator_iInter_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [CompleteLattice M] [One M] [Nonempty ι] (h1 : ⊥ = 1) (s : ι → Set α) (f : α → M) (x : α) : (⋂ (i : ι), s i).mulIndicator f x = ⨅ (i : ι), (s i).mulIndicator f x

theorem Set.indicator_iInter_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [CompleteLattice M] [Zero M] [Nonempty ι] (h1 : ⊥ = 0) (s : ι → Set α) (f : α → M) (x : α) : (⋂ (i : ι), s i).indicator f x = ⨅ (i : ι), (s i).indicator f x

theorem Set.iSup_mulIndicator {α : Type u_2} {M : Type u_3} [CompleteLattice M] [One M] {ι : Type u_4} [Preorder ι] [IsDirectedOrder ι] {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.iSup_indicator {α : Type u_2} {M : Type u_3} [CompleteLattice M] [Zero M] {ι : Type u_4} [Preorder ι] [IsDirectedOrder ι] {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.mulIndicator_le_self {α : Type u_2} {M : Type u_3} [Monoid M] [PartialOrder M] [CanonicallyOrderedMul M] (s : Set α) (f : α → M) : s.mulIndicator f ≤ f

theorem Set.indicator_le_self {α : Type u_2} {M : Type u_3} [AddMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] (s : Set α) (f : α → M) : s.indicator f ≤ f

theorem Set.mulIndicator_apply_le {α : Type u_2} {M : Type u_3} [Monoid M] [PartialOrder M] [CanonicallyOrderedMul M] {a : α} {s : Set α} {f g : α → M} (hfg : a ∈ s → f a ≤ g a) : s.mulIndicator f a ≤ g a

theorem Set.indicator_apply_le {α : Type u_2} {M : Type u_3} [AddMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {a : α} {s : Set α} {f g : α → M} (hfg : a ∈ s → f a ≤ g a) : s.indicator f a ≤ g a

theorem Set.mulIndicator_le {α : Type u_2} {M : Type u_3} [Monoid M] [PartialOrder M] [CanonicallyOrderedMul M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) : s.mulIndicator f ≤ g

theorem Set.indicator_le {α : Type u_2} {M : Type u_3} [AddMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {s : Set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) : s.indicator f ≤ g

theorem Set.mabs_mulIndicator_symmDiff {α : Type u_2} {M : Type u_3} [CommGroup M] [Lattice M] (s t : Set α) (f : α → M) (x : α) : |(symmDiff s t).mulIndicator f x|ₘ = |s.mulIndicator f x / t.mulIndicator f x|ₘ

theorem Set.abs_indicator_symmDiff {α : Type u_2} {M : Type u_3} [AddCommGroup M] [Lattice M] (s t : Set α) (f : α → M) (x : α) : |(symmDiff s t).indicator f x| = |s.indicator f x - t.indicator f x|