finite_mul — Mathlib

English

In a cancellative monoid, s * t is finite iff (s and t finite) or either s or t is empty.

Русский

В моноиде с свойством отмены, s * t конечно тогда, когда (s и t) конечно или одно из множеств пусто.

LaTeX

$$$$ (s * t).Finite \\leftrightarrow (s.Finite \\land t.Finite) \\lor (s = \\varnothing) \\lor (t = \\varnothing) $$$$

Lean4

@[to_additive]
theorem finite_mul : (s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ :=
  finite_image2 (fun _ _ ↦ (mul_left_injective _).injOn) fun _ _ ↦ (mul_right_injective _).injOn

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