exists_of_liftRel_left — Mathlib

English

If H : LiftRel R s t and a ∈ s, then there exists b with b ∈ t and R a b.

Русский

Если H : LiftRel R s t и a ∈ s, то существует b, такой что b ∈ t и R a b.

LaTeX

$$$\forall R\,\forall s,t\left(H: \mathrm{LiftRel}\ R\ s\ t\right)\;\forall a\ (ha: a \in s),\ \exists b\,(b \in t) \land R \, a \, b$$$

Lean4

theorem exists_of_liftRel_left {R : α → β → Prop} {s t} (H : LiftRel R s t) {a} (h : a ∈ s) : ∃ b, b ∈ t ∧ R a b :=
  by
  let ⟨n, h⟩ := exists_get?_of_mem h
  let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
  let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd
  exact ⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩

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