mk_mem_interedges_iff — Mathlib

English

Variant of the previous membership: (a,b) ∈ interedges(r,s,t) is equivalent to (a ∈ s) ∧ (b ∈ t) ∧ r a b.

Русский

Вариант принадлежности: (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 mk_mem_interedges_iff : (a, b) ∈ interedges r s t ↔ a ∈ s ∧ b ∈ t ∧ r a b :=
  mem_interedges_iff

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