eventually_prod_self_iff — Mathlib

English

For a relation r on α, (∀ᶠ x in la × la, r(x1,x2)) holds iff ∃ t ∈ la with ∀ x,y ∈ t, r(x,y).

Русский

Для реляции r на α: существует множество t ∈ la такое, что для любых x,y ∈ t верно r(x,y) тогда и только тогда, когда ⋯.

LaTeX

$$$$(\forall^\infty x \text{ in } \mathcal{L} \times \mathcal{L}, r(x_1,x_2)) \;\iff\; \exists t \in \mathcal{L}, \forall x \in t, \forall y \in t, r(x,y).$$$$

Lean4

theorem eventually_prod_self_iff {r : α → α → Prop} :
    (∀ᶠ x in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y :=
  mem_prod_self_iff.trans <| by simp only [prod_subset_iff, mem_setOf_eq]

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