find_apply_of_mem — Mathlib

English

If i is in the carrier of v in c, then (find c ne i)i = v i.

Русский

Если i принадлежит носителю v в c, то (find c ne i)i = v i.

LaTeX

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

Lean4

theorem find_apply_of_mem {c : Set (PartialRefinement u s p)} (hc : IsChain (· ≤ ·) c) (ne : c.Nonempty) {i v}
    (hv : v ∈ c) (hi : i ∈ carrier v) : find c ne i i = v i :=
  apply_eq_of_chain hc (find_mem _ _) hv ((mem_find_carrier_iff _).2 <| mem_iUnion₂.2 ⟨v, hv, hi⟩) hi

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