support_rangeIcc_subset — Mathlib

English

The support of f.rangeIcc g is contained in the union of supports of f and g.

Русский

Поддержка f.rangeIcc g ⊆ подмножество объединения поддержек f и g.

LaTeX

$$rangeIcc_support_subset : (f.rangeIcc g).support ⊆ f.support ∪ g.support$$

Lean4

theorem support_rangeIcc_subset [DecidableEq ι] [∀ i, DecidableEq (α i)] :
    (f.rangeIcc g).support ⊆ f.support ∪ g.support :=
  by
  refine fun x hx => ?_
  by_contra h
  refine notMem_support_iff.2 ?_ hx
  rw [rangeIcc_apply, notMem_support_iff.1 (notMem_mono subset_union_left h),
    notMem_support_iff.1 (notMem_mono subset_union_right h)]
  exact Icc_self _

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