infinite_div — Mathlib

English

For sets S,T ⊆ α in a group, the quotient S / T is infinite if and only if either S is infinite and T is nonempty, or T is infinite and S is nonempty.

Русский

Для множеств S,T ⊆ α в группе частное S / T бесконечно тогда и только тогда, когда либо S бесконечно и T непусто, либо T бесконечно и S непусто.

LaTeX

$$$(S/T).Infinite \\iff (S.Infinite \\land T.Nonempty) \\lor (T.Infinite \\land S.Nonempty)$$$

Lean4

@[to_additive]
theorem infinite_div : (s / t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty :=
  infinite_image2 (fun _ _ ↦ div_left_injective.injOn) fun _ _ ↦ div_right_injective.injOn

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