mem_interedges_iff — Mathlib

English

An ordered pair (a,b) belongs to interedges(r,s,t) exactly when a ∈ s, b ∈ t, and r a b holds.

Русский

Пара (a,b) принадлежит interedges(r,s,t) тогда и только тогда, когда a ∈ s, b ∈ t и r a b выполняется.

LaTeX

$$$ (a,b) \in \mathrm{interedges}(r,s,t) \iff a \in s \wedge b \in t \wedge r a b $$$

Lean4

theorem mem_interedges_iff {x : α × β} : x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2 := by
  rw [interedges, mem_filter, Finset.mem_product, and_assoc]

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