mem_smulAntidiagonal — Mathlib

English

For G, P with a scalar action and sets s ⊆ G, t ⊆ P, a ∈ P, an element x ∈ G × P belongs to smulAntidiagonal s t a iff x.1 ∈ s, x.2 ∈ t and x.1 • x.2 = a.

Русский

Для групп G и множества P с действием, а ∈ P и множества s ⊆ G, t ⊆ P, точка x ∈ G × P принадлежит smulAntidiagonal s t a тогда, когда x.1 ∈ s, x.2 ∈ t и x.1 • x.2 = a.

LaTeX

$$x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a$$

Lean4

@[to_additive (attr := simp)]
theorem mem_smulAntidiagonal : x ∈ smulAntidiagonal s t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a :=
  Iff.rfl

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