mem_of_le

Mathlib.Data.Multiset.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.mem_of_le

English

If s ≤ t, then a ∈ s → a ∈ t.

Русский

Если s ≤ t, то a ∈ s ⇒ a ∈ t.

LaTeX

$$$$\text{(h: } s \le t) \Rightarrow (a \in s \Rightarrow a \in t)$$$$

Lean4

theorem mem_of_le (h : s ≤ t) : a ∈ s → a ∈ t :=
  mem_of_subset (subset_of_le h)

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

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

Разделы

Аффилиация

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