mulIndicator_le_mulIndicator_apply_of_subset

English

Let s ⊆ t be subsets of α, and f: α → M with f(a) ≥ 1. Then at a, mulIndicator s f a ≤ mulIndicator t f a.

Русский

Пусть s ⊆ t — подмножества множества α, и f: α → M удовлетворяет f(a) ≥ 1. Тогда в точке a выполняется mulIndicator s f a ≤ mulIndicator t f a.

LaTeX

$$$s \subseteq t \land 1 \le f(a) \Rightarrow mulIndicator\, s\, f\, a \le mulIndicator\, t\, f\, a$$$

Lean4

@[to_additive]
theorem mulIndicator_le_mulIndicator_apply_of_subset (h : s ⊆ t) (hf : 1 ≤ f a) :
    mulIndicator s f a ≤ mulIndicator t f a :=
  mulIndicator_apply_le' (fun ha ↦ le_mulIndicator_apply (fun _ ↦ le_rfl) fun hat ↦ (hat <| h ha).elim) fun _ ↦
    one_le_mulIndicator_apply fun _ ↦ hf

Похожие утверждения