apply — Mathlib

English

The action of subtypeCongr on an element a ∈ ε is given by the explicit case split, depending on p(a).

Русский

Действие subtypeCongr на элементе a ∈ ε задаётся разбиением по условию p(a).

LaTeX

$$$ ep.subtypeCongr en(a) = \\begin{cases} ep(\\langle a, h\\rangle) & p(a) \\\\ en(\\langle a, h\\rangle) & \\neg p(a) \\end{cases} $$$

Lean4

theorem apply (a : ε) : ep.subtypeCongr en a = if h : p a then (ep ⟨a, h⟩ : ε) else en ⟨a, h⟩ := by
  by_cases h : p a <;> simp [Perm.subtypeCongr, h]

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