subset

Mathlib.Combinatorics.Additive.Dissociation

URI: https://scilib.ai/kg/mathlib#MulDissociated.subset

English

If s ⊆ t and t is MulDissociated, then s is MulDissociated.

Русский

Если s ⊆ t и t MulDissociated, то s MulDissociated.

LaTeX

$$$$ s \subseteq t \quad\Rightarrow\quad \mathrm{MulDissociated}(t) \Rightarrow \mathrm{MulDissociated}(s). $$$$

Lean4

@[to_additive]
theorem subset {t : Set α} (hst : s ⊆ t) (ht : MulDissociated t) : MulDissociated s :=
  ht.mono fun _ ↦ hst.trans'

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

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

Разделы

Аффилиация

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