existsUnique_mem — Mathlib

English

For every a ∈ s there exists a unique t ∈ P.parts with a ∈ t.

Русский

Для каждого a ∈ s существует единственная часть t ∈ P.parts, содержащая a.

LaTeX

$$$ a \in s \Rightarrow \exists! t \in P.parts, a \in t $$$

Lean4

theorem existsUnique_mem (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t :=
  by
  obtain ⟨t, ht, ht'⟩ := P.exists_mem ha
  refine ⟨t, ⟨ht, ht'⟩, ?_⟩
  rintro u ⟨hu, hu'⟩
  exact P.eq_of_mem_parts hu ht hu' ht'

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