vertices_eq — Mathlib

English

The set of vertices of K is the union, over all faces of K, of the underlying sets of those faces.

Русский

Множество вершин K есть объединение по всем граням K их множеств-оснований.

LaTeX

$$K.vertices = \\bigcup_{k \\in K.faces} (k : Set E)$$

Lean4

theorem vertices_eq : K.vertices = ⋃ k ∈ K.faces, (k : Set E) :=
  by
  ext x
  refine ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => ?_⟩
  obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h
  exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_ne_empty _)

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