exists_of_liftRel_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_of_liftRel_right {R : α → β → Prop} {s t} (H : LiftRel R s t) {b} (h : b ∈ t) : ∃ a, a ∈ s ∧ R a b := by
  rw [← LiftRel.swap] at H; exact exists_of_liftRel_left H h

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