refl

Mathlib.SetTheory.Lists

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

English

If l1 ⊆ l2 and a ∈ l1.toList, then a ∈ l2.

Русский

Если l1 ⊆ l2 и a принадлежит l1.toList, то a принадлежит l2.

LaTeX

$$$(l_1 \\subseteq l_2) \\wedge (a \\in l_1.toList) \\implies (a \\in l_2)$$$

Lean4

@[refl]
theorem refl {l : Lists' α true} : l ⊆ l := by rw [← Lists'.of_toList l]; exact ofList_subset (List.Subset.refl _)

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

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

Разделы

Аффилиация

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