English
Let α be a locally finite order and β a preorder. Antitone f iff ∀ a b, a ⋖ b → f(b) ≤ f(a).
Русский
Пусть α — локально конечный порядок, β — предпорядок. Антитонная f эквивалентна тому, что для всех a,b, где a покрывается b, выполняется f(b) ≤ f(a).
LaTeX
$$$\operatorname{Antitone}(f) \iff \forall a,b\in \alpha\, (a \prec b) \Rightarrow f(b) \le f(a)$$$
Lean4
@[simp]
theorem card_box_succ (n : ℕ) :
#(box (n + 1) : Finset (α × β)) =
#(Icc (-n.succ : α) n.succ) * #(Icc (-n.succ : β) n.succ) - #(Icc (-n : α) n) * #(Icc (-n : β) n) :=
by
rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod, Finset.card_Icc_prod]
simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg, fst_one, fst_natCast,
snd_add, snd_neg, snd_one, snd_natCast]
