univ_mul — Mathlib

English

For any t nonempty, univ * t = univ.

Русский

Для любого непустого t объединённый множитель слева равен объединённому множеству.

LaTeX

$$$ t.Nonempty \rightarrow (univ : Set α) * t = univ $$$

Lean4

@[to_additive (attr := simp)]
theorem univ_mul (ht : t.Nonempty) : (univ : Set α) * t = univ :=
  let ⟨a, ha⟩ := ht
  eq_univ_of_forall fun b => ⟨b * a⁻¹, trivial, a, ha, inv_mul_cancel_right ..⟩

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