subset_right — Mathlib

English

If B1 ⊆ B2 and CovBySMul M K A B1 holds, then CovBySMul M K A B2 holds; i.e., enlarging the right set preserves the covering relation.

Русский

Если B1 ⊆ B2 и CovBySMul M K A B1 выполнено, то CovBySMul M K A B2 выполняется; т. к. расширение правого множества сохраняет покрытие.

LaTeX

$$$$ B_1 \subseteq B_2 \quad\Rightarrow\quad \mathrm{CovBySMul}(M,K,A,B_1) \Rightarrow \mathrm{CovBySMul}(M,K,A,B_2). $$$$

Lean4

@[to_additive]
theorem subset_right (hB : B₁ ⊆ B₂) (hAB : CovBySMul M K A B₁) : CovBySMul M K A B₂ := by
  simpa using hAB.trans (.of_subset (M := M) hB)

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