mem_of_subset — Mathlib

English

Let s1 and s2 be finite subsets of a set and a be an element; if s1 is contained in s2 and a belongs to s1, then a belongs to s2.

Русский

Пусть S1 и S2 — конечные подмножества множества, и a — элемент. Если S1 ⊆ S2 и a ∈ S1, тогда a ∈ S2.

LaTeX

$$$\forall s_1,s_2:\ Finset\ α,\ \forall a:\alpha,\ s_1 \subseteq s_2 \to a \in s_1 \to a \in s_2$$$

Lean4

@[gcongr]
theorem mem_of_subset {s₁ s₂ : Finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
  Multiset.mem_of_subset

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