Theorems · Theorem · logic and foundations

Set.Pairwise.of_refl

∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Alias of the forward direction of Set.pairwise_iff_of_refl.

Defined in

Mathlib.Data.Set.Pairwise.Basic

Cited by

17 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.Refl