Antidiagonal for scalar multiplication

Given partially ordered sets G and P, with an action of G on P, we construct, for any element a in P and subsets s in G and t in P, the set of all pairs of an element in s and an element in t that scalar-multiply to a.

Definitions

• SMul.antidiagonal : Set-valued antidiagonal for SMul.
• VAdd.antidiagonal : Set-valued antidiagonal for VAdd.

def Set.smulAntidiagonal {G : Type u_1} {P : Type u_2} [SMul G P] (s : Set G) (t : Set P) (a : P) : Set (G × P)

smulAntidiagonal s t a is the set of all pairs of an element in s and an element in t that scalar multiply to a.

Equations

• s.smulAntidiagonal t a = {x : G × P | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a}

def Set.vaddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] (s : Set G) (t : Set P) (a : P) : Set (G × P)

vaddAntidiagonal s t a is the set of all pairs of an element in s and an element in t that vector-add to a.

Equations

• s.vaddAntidiagonal t a = {x : G × P | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a}

@[simp]

theorem Set.mem_smulAntidiagonal {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t : Set P} {a : P} {x : G × P} : x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

@[simp]

theorem Set.mem_vaddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} {a : P} {x : G × P} : x ∈ s.vaddAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a

theorem Set.smulAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [SMul G P] {s₁ s₂ : Set G} {t : Set P} {a : P} (h : s₁ ⊆ s₂) : s₁.smulAntidiagonal t a ⊆ s₂.smulAntidiagonal t a

theorem Set.vaddAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [VAdd G P] {s₁ s₂ : Set G} {t : Set P} {a : P} (h : s₁ ⊆ s₂) : s₁.vaddAntidiagonal t a ⊆ s₂.vaddAntidiagonal t a

theorem Set.smulAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t₁ t₂ : Set P} {a : P} (h : t₁ ⊆ t₂) : s.smulAntidiagonal t₁ a ⊆ s.smulAntidiagonal t₂ a

theorem Set.vaddAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t₁ t₂ : Set P} {a : P} (h : t₁ ⊆ t₂) : s.vaddAntidiagonal t₁ a ⊆ s.vaddAntidiagonal t₂ a

theorem Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [SMul G P] {x y : ↑(s.smulAntidiagonal t a)} [IsCancelSMul G P] : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

theorem Set.VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)} [IsCancelVAdd G P] : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

theorem Set.SMulAntidiagonal.eq_of_fst_eq_fst {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [SMul G P] {x y : ↑(s.smulAntidiagonal t a)} [IsLeftCancelSMul G P] (h : (↑x).1 = (↑y).1) : x = y

theorem Set.VAddAntidiagonal.eq_of_fst_eq_fst {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)} [IsLeftCancelVAdd G P] (h : (↑x).1 = (↑y).1) : x = y

theorem Set.SMulAntidiagonal.finite_of_finite_fst {G : Type u_1} {P : Type u_2} {s : Set G} [SMul G P] [IsLeftCancelSMul G P] (hs : s.Finite) (t : Set P) (p : P) : (s.smulAntidiagonal t p).Finite

theorem Set.VAddAntidiagonal.finite_of_finite {G : Type u_1} {P : Type u_2} {s : Set G} [VAdd G P] [IsLeftCancelVAdd G P] (hs : s.Finite) (t : Set P) (p : P) : (s.vaddAntidiagonal t p).Finite

theorem Set.SMulAntidiagonal.eq_of_snd_eq_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [SMul G P] {x y : ↑(s.smulAntidiagonal t a)} [IsCancelSMul G P] (h : (↑x).2 = (↑y).2) : x = y

theorem Set.VAddAntidiagonal.eq_of_snd_eq_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)} [IsCancelVAdd G P] (h : (↑x).2 = (↑y).2) : x = y

theorem Set.SMulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {x y : ↑(s.smulAntidiagonal t a)} (h₁ : (↑x).1 ≤ (↑y).1) (h₂ : (↑x).2 ≤ (↑y).2) : x = y

theorem Set.VAddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {x y : ↑(s.vaddAntidiagonal t a)} (h₁ : (↑x).1 ≤ (↑y).1) (h₂ : (↑x).2 ≤ (↑y).2) : x = y

theorem Set.SMulAntidiagonal.finite_of_isPWO {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] (hs : s.IsPWO) (ht : t.IsPWO) (a : P) : (s.smulAntidiagonal t a).Finite

theorem Set.VAddAntidiagonal.finite_of_isPWO {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] (hs : s.IsPWO) (ht : t.IsPWO) (a : P) : (s.vaddAntidiagonal t a).Finite