zero_mem_smul_iff — Mathlib

English

Characterization of when 0 belongs to a smul Finset in terms of membership conditions for s and t.

Русский

Характеризация принадлежности нуля смула Finset через членство в s и t.

LaTeX

$$$(0 \in s \cdot t) \iff ((0 \in s) \land t.Nonempty) \lor ((0 \in t) \land s.Nonempty)$$$

Lean4

theorem zero_mem_smul_iff : (0 : β) ∈ s • t ↔ (0 : α) ∈ s ∧ t.Nonempty ∨ (0 : β) ∈ t ∧ s.Nonempty := by
  rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]; rfl

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