mem_inter_iff

Mathlib.Data.Set.Basic

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

English

For any x, x ∈ a ∩ b iff x ∈ a and x ∈ b.

Русский

Для любого x: x ∈ a ∩ b тогда и только тогда, когда x ∈ a и x ∈ b.

LaTeX

$$$x \in a \cap b \iff x \in a \land x \in b$$$

Lean4

@[simp, mfld_simps, grind =]
theorem mem_inter_iff (x : α) (a b : Set α) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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