apply_eq_of_chain — Mathlib

English

If i belongs to the carrier of v in a chain, then the value of find at i equals v(i).

Русский

Если i принадлежит носителю v в цепи, то значение find на i равно v(i).

LaTeX

$$Eq((PartialRefinement.find c ne i).toFun i, v.toFun i)$$

Lean4

/-- If two partial refinements `v₁`, `v₂` belong to a chain (hence, they are comparable)
and `i` belongs to the carriers of both partial refinements, then `v₁ i = v₂ i`. -/
theorem apply_eq_of_chain {c : Set (PartialRefinement u s p)} (hc : IsChain (· ≤ ·) c) {v₁ v₂} (h₁ : v₁ ∈ c)
    (h₂ : v₂ ∈ c) {i} (hi₁ : i ∈ v₁.carrier) (hi₂ : i ∈ v₂.carrier) : v₁ i = v₂ i :=
  (hc.total h₁ h₂).elim (fun hle => hle.2 _ hi₁) (fun hle => (hle.2 _ hi₂).symm)

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