pairwise_subtype_iff_pairwise_finset'

English

Let r be a relation on β and f: α → β. Then Pairwise (r on fun x : s => f x) is equivalent to (s : Set α).Pairwise (r on f).

Русский

Пусть r — отношение на β и имеется отображение f: α → β. Тогда попарная совместимость (r на x ↦ f x) на s эквивалентна попарной совместимости (r на f) на подмножестве α.

LaTeX

$$$\\mathrm{Pairwise}\\bigl( r\\ on\\ \\lambda x: s. f x\\bigr) \\iff (s:\\mathrm{Set}\\alpha).\\mathrm{Pairwise}( r\\ on\\ f)$$$

Lean4

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

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