subset_left — Mathlib

English

If A1 ⊆ A2 and CovBySMul M K A2 B holds, then CovBySMul M K A1 B holds; i.e., restricting the left set preserves the covering relation.

Русский

Если A1 ⊆ A2 и CovBySMul M K A2 B, то CovBySMul M K A1 B; то есть сужение левого множества сохраняет свойство покрытия.

LaTeX

$$$$ A_1 \subseteq A_2 \quad\Rightarrow\quad \mathrm{CovBySMul}(M,K,A_2,B) \Rightarrow \mathrm{CovBySMul}(M,K,A_1,B). $$$$

Lean4

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

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