cardGe — Mathlib

English

There exists a sentence asserting that a structure has at least n elements that are pairwise distinct.

Русский

Существует предложение, утверждающее, что структура имеет не менее n попарно различныx элементов.

LaTeX

$$$\\\\exists x_1\\\\dots x_n\\\\bigwedge_{1 \\\\le i < j \\\\le n} x_i \\\\neq x_j$$$

Lean4

/-- A sentence indicating that a structure has `n` distinct elements. -/
protected def cardGe (n : ℕ) : L.Sentence :=
  ((((List.finRange n ×ˢ List.finRange n).filter fun ij : _ × _ => ij.1 ≠ ij.2).map fun ij : _ × _ =>
          ∼((&ij.1).bdEqual &ij.2)).foldr
      (· ⊓ ·) ⊤).exs

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