mem_part_iff_exists — 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_exists {b} : a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p :=
  by
  constructor
  · intro h
    have : b ∈ s := P.part_nonempty.1 ⟨a, h⟩
    refine ⟨_, ?_, h, ?_⟩ <;> simp [this]
  · rintro ⟨p, hp, hap, hbp⟩
    obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp
    exact hap

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