mem_inter — Mathlib

English

An element a belongs to s ∩ t exactly when a belongs to both s and t: a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t.

Русский

Элемент a принадлежит s ∩ t тогда и только тогда, когда a принадлежит и s, и t.

LaTeX

$$$a \\in s \\cap t \\iff a \\in s \\land a \\in t.$$$

Lean4

@[simp]
theorem mem_inter : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t :=
  ⟨fun h => ⟨mem_of_le inter_le_left h, mem_of_le inter_le_right h⟩, fun ⟨h₁, h₂⟩ => by
    rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩

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