Mathlib.AlgebraicTopology.SimplicialSet._auxLemma.4
theorem Mathlib.AlgebraicTopology.SimplicialSet._auxLemma.4 : ∀ {p q : Prop}, (¬(p ∨ q)) = (¬p ∧ ¬q)
This theorem, `Mathlib.AlgebraicTopology.SimplicialSet._auxLemma.4`, is a statement in propositional logic. It asserts that for any two propositions `p` and `q`, the negation of the disjunction (`p ∨ q`) is logically equivalent to the conjunction of their individual negations (`¬p ∧ ¬q`). In other words, "not (p or q)" is the same as "not p and not q".
More concisely: The theorem asserts that the negation of the disjunction of two propositions is logically equivalent to the conjunction of their individual negations. In mathematical notation, ¬(p ∨ q) ≡ ¬p ∧ ¬q.
|
SSet.horn.hom_ext
theorem SSet.horn.hom_ext :
∀ {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : SSet.horn (n + 1) i ⟶ S),
(∀ (j : Fin (n + 2)) (h : j ≠ i),
σ₁.app (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h) =
σ₂.app (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h)) →
σ₁ = σ₂
The theorem `SSet.horn.hom_ext` states that for any natural number `n`, any `i` in the set `{0, 1, ..., n+1}`, and any simplicial set `S`, if we have two morphisms `σ₁` and `σ₂` from the `i`-th horn of the `(n+1)`-th standard simplex to `S`, then these two morphisms are equal if and only if they are equal on all faces of the `i`-th horn that are not equal to `i`. Here, a face of the `i`-th horn is represented by a natural number `j` in the set `{0, 1, ..., n+1}` such that `j` is not equal to `i`.
More concisely: For any natural number n, simplicial set S, and i in {0, 1, ..., n+1}, two morphisms from the i-th horn of the (n+1)-th standard simplex to S are equal if and only if they agree on all faces j in {0, 1, ..., n+1} different from i.
|
Mathlib.AlgebraicTopology.SimplicialSet._auxLemma.3
theorem Mathlib.AlgebraicTopology.SimplicialSet._auxLemma.3 :
∀ {α : Type u} {s : Set α}, (s = Set.univ) = (Set.univ ⊆ s)
This theorem states that for any type `α` and a set `s` of that type, `s` equals the universal set of `α` if and only if the universal set of `α` is a subset of `s`. In mathematical terms, given a set `s` of elements of some type `α`, `s` is identical to the universal set of `α` (i.e., the set containing all elements of `α`) if and only if every element of the universal set is also an element of `s`.
More concisely: A set `s` of type `α` is equal to the universal set of `α` if and only if the universal set is a subset of `s`.
|