Set.indicator_nonneg
theorem Set.indicator_nonneg :
∀ {α : Type u_2} {M : Type u_4} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M},
(∀ a ∈ s, 0 ≤ f a) → ∀ (a : α), 0 ≤ s.indicator f a
The theorem `Set.indicator_nonneg` states that for any type `α`, any type `M` that is a preorder and has a zero element, any set `s` of type `α`, and any function `f` from `α` to `M`, if every element `a` in `s` satisfies the property that `0` is less than or equal to `f(a)`, then for every element `a` of type `α`, `0` is less than or equal to the result of applying the `Set.indicator` function on `s`, `f`, and `a`. In other words, if `f` is non-negative on `s`, then the indicator function of `s` with `f` is also non-negative.
More concisely: If `f : α → M` is a function from a set `α` to a preorder `M` with zero element, such that `0 ≤ f a` for all `a ∈ s`, then `0 ≤ ℱ s f a`, where `s : Set α` and `ℱ : Set (Set α → M → α → M)`.
|
Set.le_indicator_apply
theorem Set.le_indicator_apply :
∀ {α : Type u_2} {M : Type u_4} [inst : LE M] [inst_1 : Zero M] {s : Set α} {g : α → M} {a : α} {y : M},
(a ∈ s → y ≤ g a) → (a ∉ s → y ≤ 0) → y ≤ s.indicator g a
This theorem, `Set.le_indicator_apply`, asserts that for any types `α` and `M` where `M` has a less than or equal to (`LE`) and a zero structure, any set `s` of type `α`, any function `g` from `α` to `M`, and any elements `a` of type `α` and `y` of type `M`, if `y` is less than or equal to `g a` whenever `a` is in `s` and `y` is less than or equal to `0` whenever `a` is not in `s`, then `y` is less than or equal to the indicator function value `Set.indicator s g a`. In other words, the indicator function value for an element with respect to a set and a function is an upper bound for `y` under these conditions.
More concisely: For any set $s$ and function $g: \alpha \to M$ with $M$ having a LE and zero structure, if $y \leq g(a)$ for all $a \in s$ and $y \leq 0$ for all $a \notin s$, then $y \leq \operatorname{indicator}_s(g)(a)$.
|
Set.indicator_le'
theorem Set.indicator_le' :
∀ {α : Type u_2} {M : Type u_4} [inst : LE M] [inst_1 : Zero M] {s : Set α} {f g : α → M},
(∀ a ∈ s, f a ≤ g a) → (∀ a ∉ s, 0 ≤ g a) → s.indicator f ≤ g
The theorem `Set.indicator_le'` asserts that for any type `α` and a type `M` that has a less than or equal to (`LE`) relation and a zero element (`Zero`), given a set `s` of type `Set α` and two functions `f` and `g` from `α` to `M`, if every element `a` in `s` satisfies `f a ≤ g a` and for all `a` not in `s`, `0 ≤ g a`, then the indicator function of `s` with respect to `f` is less than or equal to `g`. In other words, for every element in the set, its corresponding value when passed through the function `f` or `0` for elements not in the set (as determined by `Set.indicator s f`) is always less than or equal to its corresponding value when passed through the function `g`.
More concisely: For any set `s` in type `Set α`, if for all `a` in `α`, `f a ≤ g a` holds when `a` is in `s`, and `0 ≤ g a` holds when `a` is not in `s`, then `Set.indicator s f ≤ g` holds.
|
Set.indicator_le_indicator_of_subset
theorem Set.indicator_le_indicator_of_subset :
∀ {α : Type u_2} {M : Type u_4} [inst : Preorder M] [inst_1 : Zero M] {s t : Set α} {f : α → M},
s ⊆ t → (∀ (a : α), 0 ≤ f a) → ∀ (a : α), s.indicator f a ≤ t.indicator f a
The theorem `Set.indicator_le_indicator_of_subset` states that for any type `α`, any preorder `M` with a zero, any two sets `s` and `t` of type `α`, and any function `f` mapping `α` to `M`, if `s` is a subset of `t` and every value of `f` is nonnegative, then for every element `a` of type `α`, the value of the indicator function of `s` and `f` at `a` is less than or equal to the value of the indicator function of `t` and `f` at `a`. In other words, if `s` is a subset of `t` and `f` is always nonnegative, then the value of the indicator function of `s` is never greater than the value of the indicator function of `t` for any given input.
More concisely: For any type `α`, preorder `M` with a zero, sets `s` and `t` of type `α`, and function `f : α → M` with nonnegative values, if `s` is a subset of `t`, then `indicator s x ≤ indicator t x` for all `x : α`.
|
Set.mulIndicator_apply_le'
theorem Set.mulIndicator_apply_le' :
∀ {α : Type u_2} {M : Type u_4} [inst : LE M] [inst_1 : One M] {s : Set α} {f : α → M} {a : α} {y : M},
(a ∈ s → f a ≤ y) → (a ∉ s → 1 ≤ y) → s.mulIndicator f a ≤ y
The theorem `Set.mulIndicator_apply_le'` states that for any type `α`, a type `M` that has a less than or equal to operation (`LE M`) and a multiplicative identity (`One M`), a set `s` of `α`, a function `f` from `α` to `M`, an element `a` of `α`, and a `y` of `M`, if `a` is in `s` implies that `f(a)` is less than or equal to `y` and if `a` is not in `s` implies that `1` is less than or equal to `y`, then the result of `Set.mulIndicator s f a` is less than or equal to `y`. In other words, the indicator function of a set and a function (which returns the function value if an element is in the set and `1` otherwise) at a particular point is always less than or equal to `y` given the stated conditions.
More concisely: For any set `s` of type `α`, function `f` from `α` to a type `M` with `LE M` and `One M`, if `a ∈ s` implies `f(a) ≤ y` and `a ∉ s` implies `1 ≤ y`, then `Set.mulIndicator s f a ≤ y`.
|
Set.indicator_apply_le'
theorem Set.indicator_apply_le' :
∀ {α : Type u_2} {M : Type u_4} [inst : LE M] [inst_1 : Zero M] {s : Set α} {f : α → M} {a : α} {y : M},
(a ∈ s → f a ≤ y) → (a ∉ s → 0 ≤ y) → s.indicator f a ≤ y
The theorem `Set.indicator_apply_le'` states that for any types `α` and `M`, where `M` has an order relation (`LE M`) and zero element (`Zero M`), a set `s` of type `Set α`, a function `f` from `α` to `M`, an element `a` of type `α`, and an element `y` of type `M`, if `f a` is less than or equal to `y` whenever `a` is in `s` and 0 is less than or equal to `y` whenever `a` is not in `s`, then the indicator function `Set.indicator s f a` is less than or equal to `y`. In other words, the value of the indicator function at `a` is always less than or equal to `y` under these conditions. The indicator function here is defined such that it gives the value of `f a` if `a` is in `s` and gives 0 otherwise.
More concisely: For any set `s` of type `α`, function `f` from `α` to an ordered type `M` with zero element `Zero M`, if `f a ≤ y` whenever `a ∈ s` and `0 ≤ y` whenever `a ∉ s`, then `Set.indicator s f a ≤ y`.
|
Set.le_mulIndicator_apply
theorem Set.le_mulIndicator_apply :
∀ {α : Type u_2} {M : Type u_4} [inst : LE M] [inst_1 : One M] {s : Set α} {g : α → M} {a : α} {y : M},
(a ∈ s → y ≤ g a) → (a ∉ s → y ≤ 1) → y ≤ s.mulIndicator g a
The theorem `Set.le_mulIndicator_apply` states that for any types `α` and `M`, where `M` has a less than or equal to relation (`LE M`) and a multiplicative identity (`One M`), given a set `s` of type `α`, a function `g` from `α` to `M`, elements `a` of type `α`, and `y` of type `M`, if `y` is less than or equal to `g a` whenever `a` is in `s`, and `y` is less than or equal to `1` whenever `a` is not in `s`, then `y` is less than or equal to the value returned by the `Set.mulIndicator` function when applied to `s`, `g`, and `a`. In other words, this theorem describes a property of the multiplicative indicator function over sets in terms of the less than or equal to relation.
More concisely: For any set `s` and function `g` from a type `α` to a type `M` with a less than or equal to relation and multiplicative identity, if `y` satisfies `y ≤ g(a)` for all `a` in `s` and `y ≤ 1` for all `a` not in `s`, then `y ≤ Set.mulIndicator s g a`.
|
Set.indicator_apply_nonneg
theorem Set.indicator_apply_nonneg :
∀ {α : Type u_2} {M : Type u_4} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M} {a : α},
(a ∈ s → 0 ≤ f a) → 0 ≤ s.indicator f a
The theorem `Set.indicator_apply_nonneg` states that for any type `α` and any preorder `M` with zero, given a set `s` of type `α`, a function `f` from `α` to `M`, and an element `a` of type `α`, if `a` is in the set `s` implies that `f(a)` is greater than or equal to zero, then the indicator function of `s` and `f` at `a` is also greater than or equal to zero. In simpler words, this theorem guarantees that if a function `f` applied to an element produces non-negative results for all elements in a set `s`, then the indicator function of `s` and `f`, which gives `f(a)` if `a` is in `s` and `0` otherwise, also produces a non-negative result for any given element.
More concisely: If `f: α → M` is a function with `M` a preorder having a zero, and `s ⊆ α` is a set such that `a ∈ s` implies `f(a) ≥ 0`, then `indicator s x ≥ 0` whenever `x ∈ α` and `x ∈ s`.
|
Set.indicator_le_self'
theorem Set.indicator_le_self' :
∀ {α : Type u_2} {M : Type u_4} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M},
(∀ x ∉ s, 0 ≤ f x) → s.indicator f ≤ f
The theorem `Set.indicator_le_self'` states that for any type `α`, a Preorder `M` that also has a `Zero` instance, a set `s` of `α`, and a function `f` from `α` to `M`, if for all `x` not in `s`, zero is less than or equal to `f(x)`, then the indicator function of `s` applied to `f` is less than or equal to `f`. This essentially means that the values assigned by the indicator function (which assigns `f(x)` for `x` in `s` and `0` otherwise) to each element are always less than or equal to the corresponding values assigned by the original function `f`, under the given condition.
More concisely: For any Preorder M with a Zero instance, set s, and function f from a type α to M, if f(x) ≤ 0 for all x ∈ α \ s, then χ\_s (x) ≤ f(x) for all x ∈ α, where χ\_s is the indicator function of set s.
|
Set.indicator_le_self
theorem Set.indicator_le_self :
∀ {α : Type u_2} {M : Type u_4} [inst : CanonicallyOrderedAddCommMonoid M] (s : Set α) (f : α → M),
s.indicator f ≤ f
The theorem `Set.indicator_le_self` states that for any type `α` and any canonically ordered additive commutative monoid `M`, for any set `s` of `α` and any function `f` from `α` to `M`, the indicator function of the set `s` with respect to `f` is less than or equal to `f`. In other words, for all elements `x` of type `α`, the value of `Set.indicator s f x` is always less than or equal to the value of `f x`. If `x` belongs to the set `s`, the values are equal; otherwise, the value of the indicator function is zero, which is the least element in a canonically ordered additive commutative monoid.
More concisely: For any set `s` and function `f`, the indicator function of `s` with respect to `f` in a canonically ordered additive commutative monoid is less than or equal to `f`.
|