subset_inter

Mathlib.Data.List.Lattice

URI: https://scilib.ai/kg/mathlib#List.subset_inter

← MathLib Explorer

English

If l ⊆ l1 and l ⊆ l2, then l ⊆ l1 ∩ l2.

Русский

Если l ⊆ l1 и l ⊆ l2, то l ⊆ l1 ∩ l2.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {l l_1 l_2 : List \\\\alpha}, l \\\\subseteq l_1 → l \\\\subseteq l_2 → l \\\\subseteq l_1 \\\\cap l_2$$$

Lean4

theorem subset_inter {l l₁ l₂ : List α} (h₁ : l ⊆ l₁) (h₂ : l ⊆ l₂) : l ⊆ l₁ ∩ l₂ := fun _ h =>
  mem_inter_iff.2 ⟨h₁ h, h₂ h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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