forall — Mathlib

English

If R is symmetric and l is Pairwise R, then for any x ∈ l and y ∈ l with x ≠ y, we have R x y.

Русский

Пусть R симметрично, а l — Pairwise R; тогда для любых x,y ∈ l с x ≠ y выполняется R x y.

LaTeX

$$$\\text{Symmetric}(R) \\land l\\text{.Pairwise}(R) \\Rightarrow \\forall x\\in l, \\forall y\\in l, x \\neq y \\Rightarrow R(x,y).$$$

Lean4

theorem «forall» (hR : Symmetric R) (hl : l.Pairwise R) : ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b :=
  by
  apply Pairwise.forall_of_forall
  · exact fun a b h hne => hR (h hne.symm)
  · exact fun _ _ hx => (hx rfl).elim
  · exact hl.imp (@fun a b h _ => by exact h)

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