pairwise_of_reflexive_of_forall_ne

English

If R is reflexive and whenever a,b ∈ l with a ≠ b we have R a b, then l is Pairwise R.

Русский

Если R рефлексивно и для любых a,b ∈ l с a ≠ b имеем R a b, то l является Pairwise R.

LaTeX

$$$\\operatorname{Reflexive}(R) \\land (\\forall a\\in l, \\forall b\\in l, a\\neq b \\Rightarrow R(a,b)) \\Rightarrow l\\text{.Pairwise}(R).$$$

Lean4

theorem pairwise_of_reflexive_of_forall_ne (hr : Reflexive R) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) : l.Pairwise R :=
  by
  rw [pairwise_iff_forall_sublist]
  intro a b hab
  if heq : a = b then cases heq; apply hr
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq

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