Documentation

Mathlib.Data.Set.SMulAntidiagonal

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 #

source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ“ coverage
      @[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
      source
      ๐Ÿ“ coverage
      @[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
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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] [IsCancelSMul G P] {x y : โ†‘(s.smulAntidiagonal t a)} :
      (โ†‘x).1 = (โ†‘y).1 โ†” (โ†‘x).2 = (โ†‘y).2
      source
      ๐Ÿ“ coverage
      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] [IsCancelVAdd G P] {x y : โ†‘(s.vaddAntidiagonal t a)} :
      (โ†‘x).1 = (โ†‘y).1 โ†” (โ†‘x).2 = (โ†‘y).2
      source
      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] [IsCancelSMul G P] {x y : โ†‘(s.smulAntidiagonal t a)} (h : (โ†‘x).1 = (โ†‘y).1) :
      x = y
      source
      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] [IsCancelVAdd G P] {x y : โ†‘(s.vaddAntidiagonal t a)} (h : (โ†‘x).1 = (โ†‘y).1) :
      x = y
      source
      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] [IsCancelSMul G P] {x y : โ†‘(s.smulAntidiagonal t a)} (h : (โ†‘x).2 = (โ†‘y).2) :
      x = y
      source
      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] [IsCancelVAdd G P] {x y : โ†‘(s.vaddAntidiagonal t a)} (h : (โ†‘x).2 = (โ†‘y).2) :
      x = y
      source
      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
      source
      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
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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