cons_subset — Mathlib

English

For any a and lists l1, l2, the subset relation cons(a,l1) ⊆ l2 is equivalent to a ∈ l2 and l1 ⊆ l2.

Русский

Для любых a и списков l1, l2, подмножество cons(a,l1) ⊆ l2 эквивалентно a ∈ l2 и l1 ⊆ l2.

LaTeX

$$$\\operatorname{cons}(a,l_1) \\subseteq l_2 \\;\\iff\\; a \\in l_2 \\land l_1 \\subseteq l_2$$$

Lean4

theorem cons_subset {a} {l₁ l₂ : Lists' α true} : Lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂ :=
  by
  refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
  generalize h' : Lists'.cons a l₁ = l₁' at h
  obtain - | @⟨a', _, _, _, e, m, s⟩ := h
  · cases a
    cases h'
  cases a; cases a'; cases h'; exact ⟨⟨_, m, e⟩, s⟩

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