ext_iff' — Mathlib

English

For any two simplices s and t in X.S, we have s = t if and only if there exists a witness h with s.dim = t.dim such that (s.cast h).simplex = t.simplex.

Русский

Для любых двух симплексов s и t в X.S выполняется: s = t тогда и только тогда, когда существует свидетель h с s.dim = t.dim и (s.cast h).simplex = t.simplex.

LaTeX

$$$\,s = t \iff \exists h:\, s.dim = t.dim,\ (s.cast(h).simplex) = t.simplex$$$

Lean4

theorem ext_iff' (s t : X.S) : s = t ↔ ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex :=
  ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun ⟨h₁, h₂⟩ ↦
    by
    obtain ⟨_, _, rfl⟩ := s.mk_surjective
    obtain ⟨_, _, rfl⟩ := t.mk_surjective
    aesop⟩

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