English
Let M be an L-structure and n a natural number. The sentence cardGe L n is realized in M exactly when the domain of M has cardinality at least n.
Русский
Для структуры M языка L предложение cardGe L n истинно в M тогда и только тогда, когда кардинальность домена M не меньше n, то есть в M есть по крайней мере n элементов.
LaTeX
$$$M \vDash \text{Sentence.cardGe } L\; n \iff \uparrow n \le |M|$$$
Lean4
@[simp]
theorem realize_cardGe (n) : M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M :=
by
rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
BoundedFormula.realize_exs]
simp_rw [BoundedFormula.realize_foldr_inf]
simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product, List.mem_finRange,
forall_exists_index, and_imp, List.mem_filter, true_and]
refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩
· rintro ⟨xs, h⟩
refine ⟨⟨xs, fun i j ij => ?_⟩⟩
contrapose! ij
have hij := h _ i j (by simpa using ij) rfl
simp only [BoundedFormula.realize_not, Term.realize, BoundedFormula.realize_bdEqual, Sum.elim_inr] at hij
exact hij
· rintro _ i j ij rfl
simpa using ij
