Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.3
theorem Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.3 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem states that for any type `α` and any two elements `a` and `b` of that type, the proposition that `a` is equal to `b` is the same as the proposition that `b` is equal to `a`. In other words, equality is symmetric: if `a` equals `b`, then `b` equals `a`, for all `a` and `b` of any type `α`.
More concisely: For all types `α` and elements `a` and `b` of type `α`, the proposition `a = b` is equivalent to the proposition `b = a`.
|
Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.5
theorem Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.5 :
∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β},
(G.boxProd H).Adj x y = (G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1)
This theorem states that for any two vertex tuples `x` and `y` from the Cartesian product of two simple graphs `G` and `H`, `x` and `y` are adjacent in the Cartesian product graph `G □ H` if and only if `x` and `y` satisfy one of two conditions: either the first elements of `x` and `y` are adjacent in `G` and the second elements are equal, or the second elements of `x` and `y` are adjacent in `H` and the first elements are equal.
More concisely: For two vertex tuples (x, y) from the Cartesian product of simple graphs G and H, they are adjacent in G □ H if and only if either the first components of x and y are adjacent in G or the second components are adjacent in H and their first components are equal.
|
Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.1
theorem Mathlib.Combinatorics.SimpleGraph.Prod._auxLemma.1 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a)
This theorem states that, for all propositions 'a' and 'b', the conjunction of 'a' and 'b' is equivalent to the conjunction of 'b' and 'a'. In other words, the order of the propositions in a logical "and" operation does not matter: 'a' and 'b' is the same as 'b' and 'a'. This is a demonstration of the commutative property in logic.
More concisely: The theorem asserts the commutativity of conjunction, that is, for all propositions 'a' and 'b', 'a' and 'b' is equivalent to 'b' and 'a'.
|