homothety_isOpenMap — Mathlib

English

Same as above in a refined simp-lemma form, expressing image subset via Set.image under homothety.

Русский

То же самое в уточнённой форме леммы, выражающее подмножество образа через образ Set.image при гомотетии.

LaTeX

$$∀t, Finite(t) → t ⊆ interior(s) → ∀ᶠ δ in 𝓝(1), image(Set.image((AffineMap.instFunLike R Q Q).coe (AffineMap.homothety x δ)) t) ⊆ s$$

Lean4

theorem homothety_isOpenMap (x : P) (t : R) (ht : t ≠ 0) : IsOpenMap <| homothety x t := by
  apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹) <;> intro e <;>
    simp [← AffineMap.comp_apply, ← homothety_mul, ht]

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