Subset — Mathlib

English

s ⊆ t means every element of s is an element of t.

Русский

s ⊆ t означает, что каждый элемент s принадлежит t.

LaTeX

$$$\\forall a, a \\in s \\Rightarrow a \\in t$$$

Lean4

/-- The subset relation on sets. `s ⊆ t` means that all elements of `s` are elements of `t`.

Note that you should **not** use this definition directly, but instead write `s ⊆ t`. -/
protected def Subset (s₁ s₂ : Set α) :=
  ∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂

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