English
In a locally finite ordered monoid with ExistsMulOfLE, the cardinality of Ico(1, a·b) equals the sum of cardinalities of Ico(1, a) and Ico(1, b) provided 1 ≤ a and 1 ≤ b.
Русский
В локально конечно упорядоченном моноиде с ExistsMulOfLE выполняется: |Ico(1, a·b)| = |Ico(1, a)| + |Ico(1, b)| при 1 ≤ a и 1 ≤ b.
LaTeX
$$$$ |Ico(1, a b)| = |Ico(1, a)| + |Ico(1, b)|, \quad ha:\ 1 \le a,\; hb:\ 1 \le b. $$$$
Lean4
@[to_additive]
theorem card_Ico_one_mul [ExistsMulOfLE M] (a b : M) (ha : 1 ≤ a) (hb : 1 ≤ b) :
#(Ico 1 (a * b)) = #(Ico 1 a) + #(Ico 1 b) :=
by
have : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b) := by simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]
rw [← this, Finset.card_union, Finset.card_Ico_mul_right]
simp [add_comm]
