English
For any nonempty c, i is in the carrier of find(c, ne, i) iff i is in chainSupCarrier(c).
Русский
Для любой непустой цепи i принадлежит носителю find(c, ne, i) тогда и только тогда, когда i принадлежит chainSupCarrier(c).
LaTeX
$$i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier(c)$$
Lean4
theorem mem_find_carrier_iff {c : Set (PartialRefinement u s p)} {i : ι} (ne : c.Nonempty) :
i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier c :=
by
rw [find]
split_ifs with h
· have := h.choose_spec
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)
· push_neg at h
refine iff_of_false (h _ ne.some_mem) ?_
simpa only [chainSupCarrier, mem_iUnion₂, not_exists]