torsionBySet_le_torsionBySet_of_subset

English

If s is contained in t, then the torsion by t is contained in the torsion by s: torsionBySet(R, M, t) ≤ torsionBySet(R, M, s) when s ⊆ t.

Русский

Если s ⊆ t, то торион по t содержится в торионе по s: torsionBySet(R, M, t) ≤ torsionBySet(R, M, s) при s ⊆ t.

LaTeX

$$$\text{If } s \subseteq t, \quad \mathrm{torsionBySet}\,R\,M\,t \leq \mathrm{torsionBySet}\,R\,M\,s.$$

Lean4

theorem torsionBySet_le_torsionBySet_of_subset {s t : Set R} (st : s ⊆ t) : torsionBySet R M t ≤ torsionBySet R M s :=
  sInf_le_sInf fun _ ⟨a, ha, h⟩ => ⟨a, st ha, h⟩

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