div_nonempty — Mathlib

English

The quotient set s / t is nonempty exactly when both s and t are nonempty: (s / t) ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅).

Русский

Множество деления s / t непусто тогда, когда оба множества s и t непусты: (s / t ≠ ∅) ⇔ (s ≠ ∅ ∧ t ≠ ∅).

LaTeX

$$$ (s / t) \neq \emptyset \iff (s \neq \emptyset \land t \neq \emptyset) $$$

Lean4

@[to_additive (attr := simp)]
theorem div_nonempty : (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  image2_nonempty_iff

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