mem_find_carrier_iff — Mathlib

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]

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