def Set.graph {G : Type u_1} {G' : Type u_2} (f : G → G') : Set (G × G')

Equations

• Set.graph f = {x : G × G' | ∃ (x_1 : G), (x_1, f x_1) = x}

theorem Set.graph_def {G : Type u_1} {G' : Type u_2} (f : G → G') : Set.graph f = {x : G × G' | ∃ (x_1 : G), (x_1, f x_1) = x}

theorem Set.card_graph {G : Type u_1} {G' : Type u_2} (f : G → G') : Nat.card ↑(Set.graph f) = Nat.card G

@[simp]

theorem Set.mem_graph {G : Type u_1} {G' : Type u_2} {f : G → G'} (x : G × G') : x ∈ Set.graph f ↔ f x.1 = x.2

theorem Set.fst_injOn_graph {G : Type u_1} {G' : Type u_2} (f : G → G') : Set.InjOn Prod.fst (Set.graph f)

@[simp]

theorem Set.image_fst_graph {G : Type u_1} {G' : Type u_2} {f : G → G'} : Prod.fst '' Set.graph f = Set.univ

@[simp]

theorem Set.image_snd_graph {G : Type u_1} {G' : Type u_2} {f : G → G'} : Prod.snd '' Set.graph f = f '' Set.univ

theorem Set.graph_comp {A : Type u_3} {B : Type u_4} {C : Type u_5} {f : A → B} (g : B → C) : Set.graph (g ∘ f) = (fun (p : A × B) => (p.1, g p.2)) '' Set.graph f

theorem Set.graph_nonempty {G : Type u_1} {G' : Type u_2} [Nonempty G] (f : G → G') : (Set.graph f).Nonempty

theorem Set.graph_add {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddCommGroup G'] {f : G →+ G'} {c : G × G'} : (fun (x : G × G') => c + x) '' Set.graph ⇑f = {x : G × G' | ∃ (g : G), (g, f g + (c.2 - f c.1)) = x}

def Set.equivFilterGraph {G : Type u_3} {G' : Type u_4} [AddCommGroup G] [Fintype G] [AddCommGroup G'] [Fintype G'] [DecidableEq G] [DecidableEq G'] (f : G → G') : let A := ⋯.toFinset; { x : (G × G') × G × G' // x ∈ Finset.filter (fun (x : (G × G') × G × G') => match x with | (a, a') => a + a' ∈ A) (A ×ˢ A) } ≃ ↑{x : G × G | f (x.1 + x.2) = f x.1 + f x.2}

Equations

• One or more equations did not get rendered due to their size.