inter_def — Mathlib

English

For sets s1 and s2, their intersection equals the set of elements that belong to both: s1 ∩ s2 = {a | a ∈ s1 ∧ a ∈ s2}.

Русский

Пересечение множеств s1 и s2 равно множеству элементов, принадлежащих одновременно обоим множествам: s1 ∩ s2 = {a | a ∈ s1 ∧ a ∈ s2}.

LaTeX

$$$s_1 \cap s_2 = \{a \mid a \in s_1 \land a \in s_2\}$$$

Lean4

theorem inter_def {s₁ s₂ : Set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂} :=
  rfl

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