definedAtLeft — Mathlib

Lean4
/-- The set of partial isomorphisms defined at `a : α`, together with a proof that any
partial isomorphism can be extended to one defined at `a`. -/
def definedAtLeft [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (a : α) : Cofinal (PartialIso α β)
    where
  carrier := {f | ∃ b : β, (a, b) ∈ f.val}
  isCofinal
    f := by
    obtain ⟨b, a_b⟩ := exists_across f a
    refine ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩, Finset.subset_insert _ _⟩
    rw [Finset.mem_insert] at hp hq
    rcases hp with (rfl | pf) <;> rcases hq with (rfl | qf)
    · simp only [cmp_self_eq_eq]
    · rw [cmp_eq_cmp_symm]
      exact a_b _ qf
    · exact a_b _ pf
    · exact f.prop _ pf _ qf
Похожие утверждения