smul_univ₀ — Mathlib

English

If s is a nontrivial subset of α, then s • univ = univ; i.e., a nontrivial set of scalars acts transitively on β.

Русский

Если s — нетривиальное подмножество α, то s • univ = univ; то есть нетривиальное множество скаляров действует транзитивно на β.

LaTeX

$$$ (hs : s.\Nontrivial) (β) : s \cdot \mathrm{univ} = \mathrm{univ}$$$

Lean4

theorem smul_univ₀ {s : Set α} (hs : ¬s ⊆ 0) : s • (univ : Set β) = univ :=
  let ⟨a, ha, ha₀⟩ := not_subset.1 hs
  eq_univ_of_forall fun b ↦ ⟨a, ha, a⁻¹ • b, trivial, smul_inv_smul₀ ha₀ _⟩

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