mem_mulAntidiagonal — Mathlib

English

An element x belongs to mulAntidiagonal hs ht a exactly when its first coordinate lies in s, its second in t, and their product equals a.

Русский

Элемент x принадлежит mulAntidiagonal hs ht a тогда и только тогда, когда первая координата x лежит в s, вторая — в t, и их произведение равно a.

LaTeX

$$x ∈ mulAntidiagonal hs ht a ⇔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 · x.2 = a$$

Lean4

@[to_additive (attr := simp)]
theorem mem_mulAntidiagonal : x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a := by
  simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]

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