English
In a cancellative ordered monoid with linear order and locally finite order, the cardinality of Ico(a·c, b·c) equals the cardinality of Ico(a, b) for all a ≤ b with ExistsMulOfLE M.
Русский
В касслантом упорядоченном моноиде с линейным порядком и локально конечным порядком кардинальность множества Ico(a·c, b·c) равна кардинальности Ico(a, b) при любых a ≤ b и существовании умножения слева.
LaTeX
$$$$ |Ico(a\,c, b\,c)| = |Ico(a, b)|, \quad [ExistsMulOfLE\, M]. $$$$
Lean4
@[to_additive]
theorem card_Ico_mul_right [ExistsMulOfLE M] (a b c : M) : #(Ico (a * c) (b * c)) = #(Ico a b) :=
by
have : (Ico (a * c) (b * c)) = (Ico a b).map (mulRightEmbedding c) :=
by
ext x
simp only [mem_Ico, mem_map, mulRightEmbedding_apply]
constructor
· rintro ⟨h₁, h₂⟩
obtain ⟨d, rfl⟩ := exists_mul_of_le h₁
exact ⟨a * d, ⟨by simpa using h₁, by simpa [mul_right_comm a c d] using h₂⟩, by simp_rw [mul_assoc, mul_comm]⟩
· aesop
simp [this]
