English
Given an ideal I of PartialIso α β and an element a ∈ α, if some partial function in I is defined at a on the left, there exists a pair (b,f) with b ∈ β and f ∈ I such that (a,b) lies in the graph of f.
Русский
Пусть I — идеал частичных изоморфизмов между α и β; при наличии a ∈ α и того, что в I встречается отображение, определённое слева на a, найдётся пара (b,f) с b ∈ β, f ∈ I и (a,b) ∈ график f.
LaTeX
$$$[DenselyOrdered \\\\beta] [NoMinOrder \\\\beta] [NoMaxOrder \\\\beta] [Nonempty \\\\beta] (a \\\\in \\\\alpha) (I : \\\\mathrm{Ideal}(\\\\mathrm{PartialIso}(\\\\alpha,\\\\beta))) \\\\rightarrow (\\\\exists f \\\\in I, \\\\exists b \\\\in \\\\beta, (a,b) \\\\in \\\\mathrm{val}(f)).$$$
Lean4
/-- Given an ideal which intersects `definedAtLeft β a`, pick `b : β` such that
some partial function in the ideal maps `a` to `b`. -/
def funOfIdeal [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (a : α) (I : Ideal (PartialIso α β)) :
(∃ f, f ∈ definedAtLeft β a ∧ f ∈ I) → { b // ∃ f ∈ I, (a, b) ∈ Subtype.val f } :=
Classical.indefiniteDescription _ ∘ fun ⟨f, ⟨b, hb⟩, hf⟩ ↦ ⟨b, f, hf, hb⟩
