mem_diff_singleton

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.mem_diff_singleton

English

For any s and b, a ∈ s \ {b} iff a ∈ s and a ≠ b.

Русский

Для любых s, a ∈ s \ {b} эквивалентно (a ∈ s) и (a ≠ b).

LaTeX

$$$$ a \in s \setminus \{b\} \iff (a \in s) \wedge (a \neq b). $$$$

Lean4

theorem mem_diff_singleton : a ∈ s \ { b } ↔ a ∈ s ∧ a ≠ b :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru