of_subset

Mathlib.Combinatorics.Additive.CovBySMul

URI: https://scilib.ai/kg/mathlib#CovBySMul.of_subset

English

If A is a subset of B, then CovBySMul M 1 A B holds; i.e., A is covered by one coset of B.

Русский

Если A ⊆ B, то CovBySMul M 1 A B выполняется; то есть A покрывается одной косетой B.

LaTeX

$$$$ \text{A} \subseteq \text{B} \Rightarrow \mathrm{CovBySMul}(M,1,A,B). $$$$

Lean4

@[to_additive (attr := simp)]
theorem of_subset (hAB : A ⊆ B) : CovBySMul M 1 A B :=
  ⟨1, by simpa⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru