finite_div — Mathlib

English

For a group-like α with division, (S / T) is finite if and only if either both S and T are finite, or S is empty, or T is empty.

Русский

Для группы с операцией деления: S / T конечное тогда и только тогда, когда либо S и T оба конечны, либо S пусто, либо T пусто.

LaTeX

$$$(S/T).\\Finite \\iff (S.\\Finite \\land T.\\Finite) \\lor S = \\varnothing \\lor T = \\varnothing$$$

Lean4

@[to_additive]
theorem finite_div : (s / t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ :=
  finite_image2 (fun _ _ ↦ div_left_injective.injOn) fun _ _ ↦ div_right_injective.injOn

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