mul_univ_of_one_mem — Mathlib

English

If a subset s contains 1, then s multiplied by the universal set equals the universal set: s * univ = univ.

Русский

Если 1 ∈ s, то произведение s на все элементы множества α дает все элементы α: s * univ = univ.

LaTeX

$$$(1 \in s) \Rightarrow (s * univ = univ)$$$

Lean4

@[to_additive]
theorem mul_univ_of_one_mem (hs : (1 : α) ∈ s) : s * univ = univ :=
  eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, hs, _, mem_univ _, one_mul _⟩

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