vadd_right_of_isCompact — Mathlib

English

If s ⊆ V is closed and t ⊆ P is compact, then s +ᵥ t is closed in P.

Русский

Если s ⊆ V замкнуто, а t ⊆ P компактно, то s +ᵥ t замкнуто в P.

LaTeX

$$$\\text{IsClosed}(s) \\;\\to\\; \\text{IsCompact}(t) \\Rightarrow \\text{IsClosed}(s +ᵥ t).$$$

Lean4

theorem vadd_right_of_isCompact {s : Set V} {t : Set P} (hs : IsClosed s) (ht : IsCompact t) : IsClosed (s +ᵥ t) :=
  by
  have ⟨p⟩ : Nonempty P := inferInstance
  have cont : Continuous (· -ᵥ p) := by fun_prop
  have := IsTopologicalAddTorsor.to_isTopologicalAddGroup V P
  convert (hs.add_right_of_isCompact <| ht.image cont).preimage cont
  rw [Set.eq_preimage_iff_image_eq <| by exact (Equiv.vaddConst p).symm.bijective, ← Set.image2_vadd, Set.image_image2,
    ← Set.image2_add, Set.image2_image_right]
  simp only [vadd_vsub_assoc]

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