existsUnique — Mathlib

English

Let π be a partition of a box I. Then for every point x ∈ I there exists a unique cell J ∈ π such that x ∈ J.

Русский

Пусть π — разбиение множества I на подмножества. Тогда для каждого элемента x ∈ I существует единственный элемент J ∈ π, удовлетворяющий x ∈ J.

LaTeX

$$$\\text{If } \\pi \\text{ is a partition of } I, \\ \\forall x \\in I: \\ \\exists! J \\in \\pi \\text{ with } x \\in J.$$$

Lean4

protected theorem existsUnique (h : π.IsPartition) (hx : x ∈ I) : ∃! J ∈ π, x ∈ J :=
  by
  rcases h x hx with ⟨J, h, hx⟩
  exact ExistsUnique.intro J ⟨h, hx⟩ fun J' ⟨h', hx'⟩ => π.eq_of_mem_of_mem h' h hx' hx

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