pairwise_subtype_iff_pairwise_set

English

For any set s, the pairwise condition on the subtype elements x,y ∈ s is equivalent to the pairwise condition on the underlying values x,y ∈ α with r.

Русский

Для любого множества s условие попарности на элементах подтипа эквивалентно попарности по:r на значениях x,y ∈ α.

LaTeX

$$$ (Pairwise \\lambda (x:s) (y:s), r\\, x y) \\iff s.Pairwise r $$$

Lean4

theorem pairwise_subtype_iff_pairwise_set (s : Set α) (r : α → α → Prop) :
    (Pairwise fun (x : s) (y : s) => r x y) ↔ s.Pairwise r := by
  simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff]

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