support_floorDiv_subset — Mathlib

English

For any finitely supported function f: ι → β and any a, the support of the floorDiv of f by a is contained in the support of f.

Русский

Для любого конечного по опоре отображения f: ι → β и любого a поддержка функции f ⌊/⌋ a ⊆ поддержка f.

LaTeX

$$$$(f \\lfloor/\\rfloor a).\\mathrm{support} \\subseteq f.\\mathrm{support}$$$$

Lean4

theorem support_floorDiv_subset : (f ⌊/⌋ a).support ⊆ f.support := by simp +contextual [Finset.subset_iff, not_imp_not]

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