pairwise_subtype_iff_pairwise_finset

English

Pairwise condition on a Finset can be checked via the corresponding set in α.

Русский

Условие попарности для Finset может проверяться через соответствующее множество в α.

LaTeX

$$$\\forall {\\alpha}, {s:\\mathrm{Finset}(\\alpha)}, (\\mathrm{Pairwise}\\, (r\\ on\\ x\\mapsto x.\\val)) \\iff (s:\\mathrm{Set}\\alpha).\\mathrm{Pairwise}(r)$$$

Lean4

theorem pairwise_subtype_iff_pairwise_finset (r : α → α → Prop) :
    Pairwise (r on fun x : s => x) ↔ (s : Set α).Pairwise r :=
  pairwise_subtype_iff_pairwise_finset' r id

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