mem_of_subset

Mathlib.SetTheory.Lists

URI: https://scilib.ai/kg/mathlib#Lists'.mem_of_subset

English

If l1 ⊆ l2 and a is in l1, then a is in l2.

Русский

Если l1 ⊆ l2 и a ∈ l1, то a ∈ l2.

LaTeX

$$$l_1 \\subseteq l_2 \\Rightarrow (a \\in l_1 \\Rightarrow a \\in l_2)$$$

Lean4

theorem mem_of_subset {a} {l₁ l₂ : Lists' α true} (s : l₁ ⊆ l₂) : a ∈ l₁ → a ∈ l₂
  | ⟨_, m, e⟩ => (mem_equiv_left e).2 (mem_of_subset' s m)

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

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

Разделы

Аффилиация

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