support_ceilDiv_subset — Mathlib

English

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

Русский

Для любого конечного по опоре отображения f: ι → β и любого a, поддержка f ⌈/⌉ a ⊆ поддержка f.

LaTeX

$$$$(f \\lceil/\\rceil a).\\mathrm{support} \\subseteq f.\\mathrm{support}$$$$

Lean4

theorem support_ceilDiv_subset : (f ⌈/⌉ a).support ⊆ f.support := by simp +contextual [Finset.subset_iff, not_imp_not]

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