mem_exposedPoints_iff_exposed_singleton

English

Exposed singleton equivalence: x ∈ A.exposedPoints 𝕜 iff IsExposed 𝕜 A {x}.

Русский

Экспонированность точки эквивалентна экспонированности соответствующего мульти-множества.

LaTeX

$$$$ x \in A.exposedPoints 𝕜 \iff IsExposed 𝕜 A \{ x \}. $$$$

Lean4

/-- Exposed points exactly correspond to exposed singletons. -/
theorem mem_exposedPoints_iff_exposed_singleton : x ∈ A.exposedPoints 𝕜 ↔ IsExposed 𝕜 A { x } :=
  by
  use fun ⟨hxA, l, hl⟩ _ =>
    ⟨l,
      Eq.symm <| eq_singleton_iff_unique_mem.2 ⟨⟨hxA, fun y hy => (hl y hy).1⟩, fun z hz => (hl z hz.1).2 (hz.2 x hxA)⟩⟩
  rintro h
  obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩
  rw [eq_comm, eq_singleton_iff_unique_mem] at hl
  exact ⟨hl.1.1, l, fun y hy => ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩

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