eventually_prod_self_iff' — Mathlib

English

A forward version of the previous statement; the equivalence holds with r regarded on pairs.

Русский

Форвардная версия предыдущего утверждения; эквивалентность сохраняется для пары (x,y).

LaTeX

$$$$ (\forall^\infty x \text{ in } la \times la, r x) \iff \exists t \in la, \forall x \in t, \forall y \in t, r\{fst:=x,snd:=y\}. $$$$

Lean4

/-- A version of `eventually_prod_self_iff` that is more suitable for forward rewriting. -/
theorem eventually_prod_self_iff' {r : α × α → Prop} : (∀ᶠ x in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y) :=
  Iff.symm eventually_prod_self_iff.symm

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