edge_edgeSet_of_ne — Mathlib

English

If s ≠ t, then the edge set of edge s t is exactly the singleton containing the unordered pair {s,t}.

Русский

Если s ≠ t, множество ребёр edge(s,t) состоит ровно из одного элемента — пары {s,t}.

LaTeX

$$$ \text{edge}(s,t).\text{edgeSet} = \{ \text{Sym2.mk}\{ fst := s, snd := t \} \} \quad\text{if } s \neq t$$$

Lean4

theorem edge_edgeSet_of_ne (h : s ≠ t) : (edge s t).edgeSet = {s(s, t)} := by
  rwa [edge, edgeSet_fromEdgeSet, sdiff_eq_left, Set.disjoint_singleton_left, Set.mem_setOf_eq, Sym2.isDiag_iff_proj_eq]

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