mem_part_iff_part_eq_part — Mathlib

English

For all a,b ∈ s, a ∈ P.part b iff ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p.

Русский

Для всех a,b ∈ s выполняется: a ∈ P.part b ⇔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p.

LaTeX

$$$ a \in P.part b \iff \exists p \in P.parts, a \in p \land b \in p $$$

Lean4

theorem mem_part_iff_part_eq_part {b : α} (ha : a ∈ s) (hb : b ∈ s) : a ∈ P.part b ↔ P.part a = P.part b :=
  ⟨fun c ↦ (P.part_eq_of_mem (P.part_mem.2 hb) c), fun c ↦ c ▸ P.mem_part ha⟩

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