mem_offDiag — Mathlib

English

For x ∈ α × α and s ⊆ α, x ∈ s.offDiag iff x1 ∈ s ∧ x2 ∈ s ∧ x1 ≠ x2.

Русский

Для x ∈ α × α и подмножества s: x ∈ s.offDiag тогда и только тогда x1 ∈ s, x2 ∈ s и x1 ≠ x2.

LaTeX

$$$$x \\in s.offDiag \\iff x_{1} \\in s \\land x_{2} \\in s \\land x_{1} \\neq x_{2}.$$$$

Lean4

@[simp, grind =]
theorem mem_offDiag {x : α × α} {s : Set α} : x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 :=
  Iff.rfl

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