subset — Mathlib

English

If A1 ⊆ A2 and B1 ⊆ B2 and CovBySMul M K A2 B1 holds, then CovBySMul M K A1 B2 holds; i.e., the combined left and right subset relations preserve the covering structure.

Русский

Если A1 ⊆ A2 и B1 ⊆ B2 и CovBySMul M K A2 B1, то CovBySMul M K A1 B2.

LaTeX

$$$$ (A_1 \subseteq A_2) \land (B_1 \subseteq B_2) \land \mathrm{CovBySMul}(M,K,A_2,B_1) \Rightarrow \mathrm{CovBySMul}(M,K,A_1,B_2). $$$$

Lean4

@[to_additive]
theorem subset (hA : A₁ ⊆ A₂) (hB : B₁ ⊆ B₂) (hAB : CovBySMul M K A₂ B₁) : CovBySMul M K A₁ B₂ :=
  (hAB.subset_left hA).subset_right hB

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