English
A dual statement to the previous one: for a given β and an ideal I of PartialIso α β, and an element b ∈ β, there exists a ∈ α and f ∈ I such that (a,b) lies in the graph of f.
Русский
Аналогично предыдущее утверждение: для заданного β и идеала I частичных изоморфизмов между α и β и элемента b ∈ β существует a ∈ α и f ∈ I такое, что (a,b) лежит в графе f.
LaTeX
$$$[DenselyOrdered \\\\alpha] [NoMinOrder \\\\alpha] [NoMaxOrder \\\\alpha] [Nonempty \\\\alpha] (b \\\\in \\\\beta) (I : \\\\mathrm{Ideal}(\\\\mathrm{PartialIso}(\\\\alpha,\\\\beta))) \\\\rightarrow (\\\\exists a \\\\in \\\\alpha, \\\\exists f \\\\in I, (a,b) \\\\in \\\\mathrm{val}(f)).$$$
Lean4
/-- Given an ideal which intersects `definedAtRight α b`, pick `a : α` such that
some partial function in the ideal maps `a` to `b`. -/
def invOfIdeal [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] (b : β) (I : Ideal (PartialIso α β)) :
(∃ f, f ∈ definedAtRight α b ∧ f ∈ I) → { a // ∃ f ∈ I, (a, b) ∈ Subtype.val f } :=
Classical.indefiniteDescription _ ∘ fun ⟨f, ⟨a, ha⟩, hf⟩ ↦ ⟨a, f, hf, ha⟩
