mem_of_subset' — Mathlib

English

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

Русский

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

LaTeX

$$$\forall {\alpha},\ {l_1 l_2 : Lists' \alpha true},\ (l_1 \subseteq l_2) \to (a \in l_1.toList) \Rightarrow (a \in l_2)$$$

Lean4

theorem mem_of_subset' {a} : ∀ {l₁ l₂ : Lists' α true} (_ : l₁ ⊆ l₂) (_ : a ∈ l₁.toList), a ∈ l₂
  | nil, _, Lists'.Subset.nil, h => by cases h
  | cons' a0 l0, l₂, s, h => by
    obtain - | ⟨e, m, s⟩ := s
    simp only [toList, Sigma.eta, List.mem_cons] at h
    rcases h with (rfl | h)
    · exact ⟨_, m, e⟩
    · exact mem_of_subset' s h

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