isClosed_direction_iff — Mathlib

English

Let s be an affine subspace with direction a subspace of V. If V is T1, then s is closed in P iff its direction is closed in V.

Русский

Пусть s — аффинное подпространство с направлением, являющимся подпространством V. При выполнение T1 в V, множество s замкнуто в P тогда и только тогда, когда направление замкнуто в V.

LaTeX

$$[T1Space V] ⇒ IsClosed(s.direction) ↔ IsClosed((s:Set P))$$

Lean4

theorem isClosed_direction_iff [T1Space V] (s : AffineSubspace R P) :
    IsClosed (s.direction : Set V) ↔ IsClosed (s : Set P) :=
  by
  rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩); · simp
  rw [← (Homeomorph.vaddConst x).symm.isClosed_image, AffineSubspace.coe_direction_eq_vsub_set_right hx]
  simp only [Homeomorph.vaddConst_symm_apply]

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