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]