exists_mem_of_rel_of_mem — Mathlib

English

If Rel r s t holds, then for every a ∈ s there exists b ∈ t with r a b.

Русский

Если Rel r s t выполняется, то для каждого a ∈ s существует b ∈ t с r a b.

LaTeX

$$$Rel\ r\ s\ t \rightarrow \forall a \in s, \exists b \in t, r\ a\ b$$$

Lean4

theorem exists_mem_of_rel_of_mem {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) :
    ∀ {a : α}, a ∈ s → ∃ b ∈ t, r a b := by
  induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

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