Complete bipartite graphs
Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Victor Blanchi.
Created on 2022-07-03.
Last modified on 2023-09-06.
module graph-theory.complete-bipartite-graphs where
Imports
open import foundation.coproduct-types open import foundation.universe-levels open import foundation.unordered-pairs open import graph-theory.finite-graphs open import univalent-combinatorics.2-element-types open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.fibers-of-maps open import univalent-combinatorics.finite-types
Definition
complete-bipartite-Undirected-Graph-𝔽 : {l1 l2 : Level} → 𝔽 l1 → 𝔽 l2 → Undirected-Graph-𝔽 (l1 ⊔ l2) (l1 ⊔ l2) pr1 (complete-bipartite-Undirected-Graph-𝔽 X Y) = coprod-𝔽 X Y pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p = prod-𝔽 ( Σ-𝔽 X ( λ x → fiber-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( coprod-𝔽 X Y) ( element-unordered-pair p) ( inl x))) ( Σ-𝔽 Y ( λ y → fiber-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( coprod-𝔽 X Y) ( element-unordered-pair p) ( inr y)))
Recent changes
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).